theorem
EuclidGeom.ratio_eq_ratio_perm
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{X : P}
{Y : P}
{Z : P}
(ha : EuclidGeom.Collinear A B C)
(hx : EuclidGeom.Collinear X Y Z)
(h : EuclidGeom.divratio A B C = EuclidGeom.divratio X Y Z)
:
EuclidGeom.divratio B C A = EuclidGeom.divratio Y Z X
theorem
EuclidGeom.ratio_eq_ratio_flip₁
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{X : P}
{Y : P}
{Z : P}
(ha : EuclidGeom.Collinear A B C)
(hx : EuclidGeom.Collinear X Y Z)
(h : EuclidGeom.divratio A B C = EuclidGeom.divratio X Y Z)
:
EuclidGeom.divratio A C B = EuclidGeom.divratio X Z Y
theorem
EuclidGeom.ratio_eq_ratio_flip₂
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{X : P}
{Y : P}
{Z : P}
(ha : EuclidGeom.Collinear A B C)
(hx : EuclidGeom.Collinear X Y Z)
(h : EuclidGeom.divratio A B C = EuclidGeom.divratio X Y Z)
:
EuclidGeom.divratio C B A = EuclidGeom.divratio Z Y X
theorem
EuclidGeom.ratio_eq_ratio_flip₃
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{X : P}
{Y : P}
{Z : P}
(ha : EuclidGeom.Collinear A B C)
(hx : EuclidGeom.Collinear X Y Z)
(h : EuclidGeom.divratio A B C = EuclidGeom.divratio X Y Z)
:
EuclidGeom.divratio B A C = EuclidGeom.divratio Y X Z
theorem
EuclidGeom.ratio_eq_ratio_trans
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{D : P}
{X : P}
{Y : P}
{Z : P}
{W : P}
[EuclidGeom.PtNe C D]
[EuclidGeom.PtNe Z W]
{l₁ : EuclidGeom.Line P}
{l₂ : EuclidGeom.Line P}
(ha : EuclidGeom.lies_on A l₁)
(hb : EuclidGeom.lies_on B l₁)
(hc : EuclidGeom.lies_on C l₁)
(hd : EuclidGeom.lies_on D l₁)
(hx : EuclidGeom.lies_on X l₂)
(hy : EuclidGeom.lies_on Y l₂)
(hz : EuclidGeom.lies_on Z l₂)
(hw : EuclidGeom.lies_on W l₂)
(h₁ : EuclidGeom.divratio A C D = EuclidGeom.divratio X Z W)
(h₂ : EuclidGeom.divratio B C D = EuclidGeom.divratio Y Z W)
:
EuclidGeom.divratio A B C = EuclidGeom.divratio X Y Z
theorem
EuclidGeom.Seg.midpt_ratio
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{s : EuclidGeom.Seg P}
:
EuclidGeom.divratio s.midpoint s.source s.target = -1
theorem
EuclidGeom.seg_midpt_ratio
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
(A : P)
(B : P)
:
EuclidGeom.divratio { source := A, target := B }.midpoint A B = -1
theorem
EuclidGeom.ratio_eq_of_divratio_eq
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{X : P}
{Y : P}
{Z : P}
[EuclidGeom.PtNe A C]
[EuclidGeom.PtNe X Z]
(ha : EuclidGeom.Collinear A B C)
(hx : EuclidGeom.Collinear X Y Z)
(h : EuclidGeom.divratio A B C = EuclidGeom.divratio X Y Z)
: