Add more necessary lemmas

EuclideanGeometry/Foundation/Axiom/Basic/Angle/AddToMathlib.lean

@@ -8,6 +8,7 @@ Maybe we can create some PRs to mathlib in the future.
 -/
 
 open Real Classical
+
 attribute [ext] Complex.ext
 
 /-!
@@ -980,6 +981,13 @@ theorem Real.div_nat_le_self_of_pos {a : ℝ} (n : ℕ) (h : 0 < a) : a / n ≤
 theorem Real.div_nat_lt_self_of_pos_of_two_le {a : ℝ} {n : ℕ} (h : 0 < a) (hn : 2 ≤ n) : a / n < a :=
   mul_lt_of_lt_one_right h (inv_lt_one (Nat.one_lt_cast.mpr hn))
 
+theorem Real.div_eq_div_of_div_eq_div {a b c d : ℝ} (hc : c ≠ 0) (hd : d ≠ 0) (h : a / b = c / d) : a / c = b / d := by
+  have hb : b ≠ 0 := by
+    intro hb
+    rw [hb, div_zero] at h
+    exact div_ne_zero hc hd h.symm
+  exact (div_eq_div_iff hc hd).mpr (((div_eq_div_iff hb hd).mp h).trans (mul_comm c b))
+
 theorem pi_div_nat_nonneg (n : ℕ) : 0 ≤ π / n :=
   div_nonneg (le_of_lt pi_pos) (Nat.cast_nonneg n)
 

EuclideanGeometry/Foundation/Axiom/Linear/Ratio_trash.lean

@@ -0,0 +1,24 @@
+import EuclideanGeometry.Foundation.Axiom.Linear.Ratio
+
+noncomputable section
+namespace EuclidGeom
+
+variable {P : Type*} [EuclideanPlane P] {A B C D X Y Z W : P}
+
+theorem ratio_eq_ratio_perm (ha : Collinear A B C) (hx : Collinear X Y Z) (h : divratio A B C = divratio X Y Z) : divratio B C A = divratio Y Z X := sorry
+
+theorem ratio_eq_ratio_flip₁ (ha : Collinear A B C) (hx : Collinear X Y Z) (h : divratio A B C = divratio X Y Z) : divratio A C B = divratio X Z Y := sorry
+
+theorem ratio_eq_ratio_flip₂ (ha : Collinear A B C) (hx : Collinear X Y Z) (h : divratio A B C = divratio X Y Z) : divratio C B A = divratio Z Y X := sorry
+
+theorem ratio_eq_ratio_flip₃ (ha : Collinear A B C) (hx : Collinear X Y Z) (h : divratio A B C = divratio X Y Z) : divratio B A C = divratio Y X Z := sorry
+
+theorem ratio_eq_ratio_trans [PtNe C D] [PtNe Z W] {l₁ l₂ : Line P} (ha : A LiesOn l₁) (hb : B LiesOn l₁) (hc : C LiesOn l₁) (hd : D LiesOn l₁) (hx : X LiesOn l₂) (hy : Y LiesOn l₂) (hz : Z LiesOn l₂) (hw : W LiesOn l₂) (h₁ : divratio A C D = divratio X Z W) (h₂ : divratio B C D = divratio Y Z W) : divratio A B C = divratio X Y Z := sorry
+
+theorem Seg.midpt_ratio {s : Seg P} : divratio s.midpoint s.source s.target = - 1 := sorry
+
+theorem seg_midpt_ratio (A B : P) : divratio (SEG A B).midpoint A B = - 1 := sorry
+
+theorem ratio_eq_of_divratio_eq [PtNe A C] [PtNe X Z] (ha : Collinear A B C) (hx : Collinear X Y Z) (h : divratio A B C = divratio X Y Z) : dist A B / dist A C = dist X Y / dist X Z := sorry
+
+end EuclidGeom

EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean

@@ -1566,6 +1566,10 @@ theorem Seg.dist_target_eq_dist_source_of_midpt {seg : Seg P} : (SEG seg.source
   rw [Seg.length_eq_norm_toVec, Seg.length_eq_norm_toVec]
   exact congrArg norm seg.vec_midpt_eq
 
+/-- The midpoint of a segment has same distance to the source and to the target of the segment. -/
+theorem Seg.dist_target_eq_dist_source_of_midpt' {seg : Seg P} : (SEG seg.midpoint seg.source).length = (SEG seg.midpoint seg.target).length :=
+  ((SEG seg.source seg.midpoint).length_of_rev_eq_length).trans seg.dist_target_eq_dist_source_of_midpt
+
 /-- The midpoint of a segment has same distance to the source and to the target of the segment. -/
 theorem Seg.dist_target_eq_dist_source_of_eq_midpt {X : P} {seg : Seg P} (h : X = seg.midpoint) : (SEG seg.1 X).length = (SEG X seg.2).length := by
   rw [h]

EuclideanGeometry/Foundation/Axiom/Position/Angle.lean

@@ -565,6 +565,17 @@ theorem mk_start_dirLine_end_dirLine_eq_self_of_isND (h : ang.IsND): mk_dirline_
     (Eq.symm <| inx_of_line_eq_inx (start_dirLine_not_para_end_dirLine_of_value_ne_zero h)
       ⟨ang.source_lies_on_start_dirLine, ang.source_lies_on_end_dirLine⟩) rfl rfl
 
+theorem dvalue_eq_of_lies_on_line {A B : P} [PtNe A ang.source] [PtNe B ang.source] (ha : A LiesOn ang.start_ray.toLine) (hb : B LiesOn ang.end_ray.toLine) : ∡ A ang.source B = ang.dvalue := by
+  show (SEG_nd ang.1 B).toProj -ᵥ (SEG_nd ang.1 A).toProj = ang.dvalue
+  rw [ang.start_ray.toLine.toProj_eq_seg_nd_toProj_of_lies_on source_lies_on_start_dirLine ha]
+  rw [ang.end_ray.toLine.toProj_eq_seg_nd_toProj_of_lies_on source_lies_on_end_dirLine hb]
+  rfl
+
+theorem dvalue_eq_of_lies_on_line_pt_pt {A B C D O : P} [_ha : PtNe A O] [_hb : PtNe B O] [_hc : PtNe C O] [_hd : PtNe D O] (hc : C LiesOn (LIN O A)) (hd : D LiesOn (LIN O B)) : ∡ C O D = ∡ A O B :=
+  haveI : PtNe C (ANG A O B).source := _hc
+  haveI : PtNe D (ANG A O B).source := _hd
+  (ANG A O B).dvalue_eq_of_lies_on_line hc hd
+
 end mk_compatibility
 
 section cancel
@@ -689,7 +700,7 @@ theorem dir_perp_iff_dvalue_eq_pi_div_two : ang.dir₁ ⟂ ang.dir₂ ↔ ang.dv
   nth_rw 1 [← AngDValue.neg_coe_pi_div_two, ← neg_vsub_eq_vsub_rev]
   exact neg_inj
 
-theorem line_pt_pt_perp_iff_dvalue_eq_pi_div_two : LIN O A ⟂ LIN O B ↔ (ANG A O B).dvalue = ∡[π / 2] :=
+theorem line_pt_pt_perp_iff_dvalue_eq_pi_div_two : LIN O A ⟂ LIN O B ↔ ∡ A O B = ∡[π / 2] :=
   (ANG A O B).dir_perp_iff_dvalue_eq_pi_div_two
 
 theorem dir_perp_iff_isRt : ang.dir₁ ⟂ ang.dir₂ ↔ ang.IsRt :=
@@ -701,7 +712,7 @@ theorem line_pt_pt_perp_iff_isRt : LIN O A ⟂ LIN O B ↔ (ANG A O B).IsRt :=
 theorem value_eq_pi_of_lies_int_seg_nd {A B C : P} [PtNe C A] (h : B LiesInt (SEG_nd A C)) : ∠ A B C h.2.symm h.3.symm = π :=
   value_eq_pi_of_eq_neg_dir ((SEG_nd A C).toDir_eq_neg_toDir_of_lies_int h)
 
-theorem collinear_iff_dvalue_eq_zero : Collinear O A B ↔ (ANG A O B).dvalue = 0 :=
+theorem collinear_iff_dvalue_eq_zero : Collinear O A B ↔ ∡ A O B = 0 :=
   collinear_iff_toProj_eq_of_ptNe.trans (eq_comm.trans vsub_eq_zero_iff_eq.symm)
 
 theorem collinear_iff_not_isND : Collinear O A B ↔ ¬ (ANG A O B).IsND :=

EuclideanGeometry/Foundation/Axiom/Position/Angle_ex2.lean

@@ -149,15 +149,18 @@ section perp_foot
 
 variable {ang : Angle P}
 
-theorem dvalue_eq_pi_div_two_at_perp_foot {A B C : P} [_h : PtNe B C] (l : Line P) (hb : B LiesOn l) (ha : ¬ A LiesOn l) (hc : C = perp_foot A l) : haveI : PtNe A C := ⟨((pt_ne_iff_not_lies_on_of_eq_perp_foot hc).mpr ha).symm⟩; (ANG A C B).dvalue = ∡[π / 2] := by
-  haveI : PtNe A C := ⟨((pt_ne_iff_not_lies_on_of_eq_perp_foot hc).mpr ha).symm⟩
-  haveI : PtNe B (perp_foot A l) := by
-    rw [← hc]
+theorem dvalue_eq_pi_div_two_at_perp_foot {A O B : P} [_h : PtNe A O] {l : Line P} (ha : A LiesOn l) (ho : O = perp_foot B l) (hb : ¬ B LiesOn l) : haveI : PtNe B O := ⟨((pt_ne_iff_not_lies_on_of_eq_perp_foot ho).mpr hb).symm⟩; ∡ A O B = ∡[π / 2] := by
+  haveI _hbo : PtNe B O := ⟨((pt_ne_iff_not_lies_on_of_eq_perp_foot ho).mpr hb).symm⟩
+  haveI : PtNe A (perp_foot B l) := by
+    rw [← ho]
     exact _h
   apply line_pt_pt_perp_iff_dvalue_eq_pi_div_two.mp
-  rw [Line.line_of_pt_pt_eq_rev]
-  simp only [hc, Line.eq_line_of_pt_pt_of_ne (perp_foot_lies_on_line A l) hb]
-  exact line_of_self_perp_foot_perp_line_of_not_lies_on ha
+  rw [Line.line_of_pt_pt_eq_rev (_h := _hbo)]
+  simp only [ho, Line.eq_line_of_pt_pt_of_ne (perp_foot_lies_on_line B l) ha]
+  exact (line_of_self_perp_foot_perp_line_of_not_lies_on hb).symm
+
+theorem isRt_at_perp_foot {A O B : P} [_h : PtNe A O] {l : Line P} (ha : A LiesOn l) (ho : O = perp_foot B l) (hb : ¬ B LiesOn l) : haveI : PtNe B O := ⟨((pt_ne_iff_not_lies_on_of_eq_perp_foot ho).mpr hb).symm⟩; (ANG A O B).IsRt :=
+  AngValue.isRt_iff_coe.mpr (dvalue_eq_pi_div_two_at_perp_foot ha ho hb)
 
 theorem perp_foot_lies_int_start_ray_iff_isAcu {A O B : P} [PtNe A O] [PtNe B O] : (perp_foot B (LIN O A)) LiesInt (RAY O A) ↔ (ANG A O B).IsAcu := by
   refine' ((RAY O A).lies_int_iff_pos_of_vec_eq_smul_toDir

EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle.lean

@@ -1,6 +1,3 @@
-import EuclideanGeometry.Foundation.Axiom.Triangle.Basic
-import EuclideanGeometry.Foundation.Axiom.Triangle.Basic_ex
-import EuclideanGeometry.Foundation.Axiom.Triangle.Trigonometric
 import EuclideanGeometry.Foundation.Axiom.Triangle.Congruence
 
 

EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle_trash.lean

@@ -13,4 +13,6 @@ theorem ang_acute_of_is_isoceles {A B C : P} (h : ¬ Collinear A B C) (isoceles_
 
 theorem ang_acute_of_is_isoceles_variant {A B C : P} (h : ¬ Collinear A B C) (isoceles_ABC : (▵ A B C).IsIsoceles) : Angle.IsAcu (ANG A C B (ne_of_not_collinear h).2.1 (ne_of_not_collinear h).1.symm) := by sorry
 
+theorem midpt_eq_perp_foot_of_isIsoceles {A B C : P} [PtNe B C] (h : (▵ A B C).IsIsoceles) : (SEG B C).midpoint = perp_foot A (LIN B C) := sorry
+
 end EuclidGeom

EuclideanGeometry/Foundation/Axiom/Triangle/Similarity.lean

@@ -22,7 +22,7 @@ structure IsASim (tr₁ tr₂ : TriangleND P) : Prop where intro ::
 
 namespace IsSim
 
-protected theorem refl (tr : TriangleND P): IsSim tr tr where
+protected theorem refl (tr : TriangleND P) : IsSim tr tr where
   angle₁ := rfl
   angle₂ := rfl
   angle₃ := rfl
@@ -285,7 +285,7 @@ theorem asim_of_AA (tr₁ tr₂ : TriangleND P) (h₂ : tr₁.angle₂.value = -
   exact h₃
 
 /- SAS -/
-theorem sim_of_SAS (tr₁ tr₂ : TriangleND P) (e : tr₁.edge₂.length / tr₂.edge₂.length = tr₁.edge₃.length / tr₂.edge₃.length) (a : tr₁.angle₁.value = tr₂.angle₁.value): tr₁ ∼ tr₂ := by
+theorem sim_of_SAS (tr₁ tr₂ : TriangleND P) (e : tr₁.edge₂.length / tr₂.edge₂.length = tr₁.edge₃.length / tr₂.edge₃.length) (a : tr₁.angle₁.value = tr₂.angle₁.value) : tr₁ ∼ tr₂ := by
   have eq : tr₁.edge₂.length * tr₂.edge₃.length = tr₁.edge₃.length * tr₂.edge₂.length := by
     exact (div_eq_div_iff (Seg.length_ne_zero_iff_nd.mpr tr₂.edgeND₂.2).symm (Seg.length_ne_zero_iff_nd.mpr tr₂.edgeND₃.2).symm).mp e
   rw [mul_comm tr₁.edge₃.length  tr₂.edge₂.length] at eq
@@ -414,7 +414,7 @@ theorem sim_of_SAS (tr₁ tr₂ : TriangleND P) (e : tr₁.edge₂.length / tr
   apply (angle₁_neg_iff_not_cclock tr₂).mp
   exact cc
 
-theorem asim_of_SAS (tr₁ tr₂ : TriangleND P) (e : tr₁.edge₂.length / tr₂.edge₂.length = tr₁.edge₃.length / tr₂.edge₃.length) (a : tr₁.angle₁.value = - tr₂.angle₁.value): tr₁ ∼ₐ tr₂ := by
+theorem asim_of_SAS (tr₁ tr₂ : TriangleND P) (e : tr₁.edge₂.length / tr₂.edge₂.length = tr₁.edge₃.length / tr₂.edge₃.length) (a : tr₁.angle₁.value = - tr₂.angle₁.value) : tr₁ ∼ₐ tr₂ := by
   have eq : tr₁.edge₂.length * tr₂.edge₃.length = tr₁.edge₃.length * tr₂.edge₂.length := by
     exact (div_eq_div_iff (Seg.length_ne_zero_iff_nd.mpr tr₂.edgeND₂.2).symm (Seg.length_ne_zero_iff_nd.mpr tr₂.edgeND₃.2).symm).mp e
   rw [mul_comm tr₁.edge₃.length  tr₂.edge₂.length] at eq

EuclideanGeometry/Foundation/Construction/ComputationTool/Parallel.lean

@@ -8,18 +8,42 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Parallel
 noncomputable section
 namespace EuclidGeom
 
-variable {P : Type*} [EuclideanPlane P] {A B C D E F X : P} [PtNe A B] [PtNe C D] [PtNe E F]
+variable {P : Type*} [EuclideanPlane P] {l₁ l₂ l₃ : Line P} {A B C D E F X : P}
 
-theorem divratio_eq_of_para (h : (LIN A B) ∥ (LIN C D)) (hxac : Collinear X A C) (hxbd : Collinear X B D) (hn : (LIN A B) ≠ (LIN C D)) : divratio X A C = divratio X B D := sorry
+theorem divratio_eq_of_para₁₂₃ (ha : A LiesOn l₁) (hb : B LiesOn l₁) (hc : C LiesOn l₂) (hd : D LiesOn l₂) (h : l₁ ∥ l₂) (ne : l₁ ≠ l₂) (hxac : Collinear A C X) (hxbd : Collinear B D X) : divratio X A C = divratio X B D := sorry
 
-theorem divratio_eq_of_para_of_para (habcd : (LIN A B) ∥ (LIN C D)) (habef : (LIN A B) ∥ (LIN E F)) (hace : Collinear A C E) (hbdf : Collinear B D F) (hn : (LIN C D) ≠ (LIN E F)) : divratio A C E = divratio B D F := sorry
+theorem divratio_eq_of_para₁₃₂ (ha : A LiesOn l₁) (hb : B LiesOn l₁) (hc : C LiesOn l₂) (hd : D LiesOn l₂) (h : l₁ ∥ l₂) (ne : l₁ ≠ l₂) (hxac : Collinear A C X) (hxbd : Collinear B D X) : divratio X C A = divratio X D B := sorry
 
-theorem line_inx_lies_on_seg_iff_of_para (h : (LIN A B) ∥ (LIN C D)) (hxac : Collinear X A C) (hxbd : Collinear X B D) (hn : (LIN A B) ≠ (LIN C D)) : X LiesOn (SEG A C) ↔ X LiesOn (SEG B D) := sorry
+theorem divratio_eq_of_para₂₁₃ (ha : A LiesOn l₁) (hb : B LiesOn l₁) (hc : C LiesOn l₂) (hd : D LiesOn l₂) (h : l₁ ∥ l₂) (ne : l₁ ≠ l₂) (hxac : Collinear A C X) (hxbd : Collinear B D X) : divratio A X C = divratio B X D := sorry
 
-theorem line_inx_lies_int_seg_iff_of_para (h : (LIN A B) ∥ (LIN C D)) (hxac : Collinear X A C) (hxbd : Collinear X B D) (hn : (LIN A B) ≠ (LIN C D)) : X LiesInt (SEG A C) ↔ X LiesInt (SEG B D) := sorry
+theorem divratio_eq_of_para₂₃₁ (ha : A LiesOn l₁) (hb : B LiesOn l₁) (hc : C LiesOn l₂) (hd : D LiesOn l₂) (h : l₁ ∥ l₂) (ne : l₁ ≠ l₂) (hxac : Collinear A C X) (hxbd : Collinear B D X) : divratio A C X = divratio B D X := sorry
 
-theorem lies_on_seg_line_inx_iff_of_para (h : (LIN A B) ∥ (LIN C D)) (hxac : Collinear X A C) (hxbd : Collinear X B D) (hn : (LIN A B) ≠ (LIN C D)) : A LiesOn (SEG C X) ↔ B LiesOn (SEG D X) := sorry
+theorem divratio_eq_of_para₃₁₂ (ha : A LiesOn l₁) (hb : B LiesOn l₁) (hc : C LiesOn l₂) (hd : D LiesOn l₂) (h : l₁ ∥ l₂) (ne : l₁ ≠ l₂) (hxac : Collinear A C X) (hxbd : Collinear B D X) : divratio C X A = divratio D X B := sorry
 
-theorem lies_int_seg_line_inx_iff_of_para (h : (LIN A B) ∥ (LIN C D)) (hxac : Collinear X A C) (hxbd : Collinear X B D) (hn : (LIN A B) ≠ (LIN C D)) : A LiesInt (SEG C X) ↔ B LiesInt (SEG D X) := sorry
+theorem divratio_eq_of_para₃₂₁ (ha : A LiesOn l₁) (hb : B LiesOn l₁) (hc : C LiesOn l₂) (hd : D LiesOn l₂) (h : l₁ ∥ l₂) (ne : l₁ ≠ l₂) (hxac : Collinear A C X) (hxbd : Collinear B D X) : divratio C A X = divratio D B X := sorry
+
+theorem divratio_eq_of_para_of_para (ha : A LiesOn l₁) (hb : B LiesOn l₁) (hc : C LiesOn l₂) (hd : D LiesOn l₂) (he : E LiesOn l₃) (hf : F LiesOn l₃) (h₁₂ : l₁ ∥ l₂) (h₁₃ : l₁ ∥ l₃) (ne : l₁ ≠ l₂)  (hace : Collinear A C E) (hbdf : Collinear B D F) : divratio A C E = divratio B D F := sorry
+
+theorem line_inx_lies_on_seg_iff_of_para (ha : A LiesOn l₁) (hb : B LiesOn l₁) (hc : C LiesOn l₂) (hd : D LiesOn l₂) (h : l₁ ∥ l₂) (ne : l₁ ≠ l₂) (hxac : Collinear A C X) (hxbd : Collinear B D X) : X LiesOn (SEG A C) ↔ X LiesOn (SEG B D) := sorry
+
+theorem line_inx_lies_int_seg_iff_of_para (ha : A LiesOn l₁) (hb : B LiesOn l₁) (hc : C LiesOn l₂) (hd : D LiesOn l₂) (h : l₁ ∥ l₂) (ne : l₁ ≠ l₂) (hxac : Collinear A C X) (hxbd : Collinear B D X) : X LiesInt (SEG A C) ↔ X LiesInt (SEG B D) := sorry
+
+theorem lies_on_seg_line_inx_iff_of_para (ha : A LiesOn l₁) (hb : B LiesOn l₁) (hc : C LiesOn l₂) (hd : D LiesOn l₂) (h : l₁ ∥ l₂) (ne : l₁ ≠ l₂) (hxac : Collinear A C X) (hxbd : Collinear B D X) : A LiesOn (SEG C X) ↔ B LiesOn (SEG D X) := sorry
+
+theorem lies_int_seg_line_inx_iff_of_para (ha : A LiesOn l₁) (hb : B LiesOn l₁) (hc : C LiesOn l₂) (hd : D LiesOn l₂) (h : l₁ ∥ l₂) (ne : l₁ ≠ l₂) (hxac : Collinear A C X) (hxbd : Collinear B D X) : A LiesInt (SEG C X) ↔ B LiesInt (SEG D X) := sorry
+
+variable [PtNe A B] [PtNe C D] [PtNe E F]
+
+theorem divratio_eq_of_para' (h : (LIN A B) ∥ (LIN C D)) (hxac : Collinear A C X) (hxbd : Collinear B D X) (hn : (LIN A B) ≠ (LIN C D)) : divratio X A C = divratio X B D := sorry
+
+theorem divratio_eq_of_para_of_para' (habcd : (LIN A B) ∥ (LIN C D)) (habef : (LIN A B) ∥ (LIN E F)) (hace : Collinear A C E) (hbdf : Collinear B D F) (hn : (LIN A B) ≠ (LIN C D)) : divratio A C E = divratio B D F := sorry
+
+theorem line_inx_lies_on_seg_iff_of_para' (h : (LIN A B) ∥ (LIN C D)) (hxac : Collinear A C X) (hxbd : Collinear B D X) (hn : (LIN A B) ≠ (LIN C D)) : X LiesOn (SEG A C) ↔ X LiesOn (SEG B D) := sorry
+
+theorem line_inx_lies_int_seg_iff_of_para' (h : (LIN A B) ∥ (LIN C D)) (hxac : Collinear A C X) (hxbd : Collinear B D X) (hn : (LIN A B) ≠ (LIN C D)) : X LiesInt (SEG A C) ↔ X LiesInt (SEG B D) := sorry
+
+theorem lies_on_seg_line_inx_iff_of_para' (h : (LIN A B) ∥ (LIN C D)) (hxac : Collinear A C X) (hxbd : Collinear B D X) (hn : (LIN A B) ≠ (LIN C D)) : A LiesOn (SEG C X) ↔ B LiesOn (SEG D X) := sorry
+
+theorem lies_int_seg_line_inx_iff_of_para' (h : (LIN A B) ∥ (LIN C D)) (hxac : Collinear A C X) (hxbd : Collinear B D X) (hn : (LIN A B) ≠ (LIN C D)) : A LiesInt (SEG C X) ↔ B LiesInt (SEG D X) := sorry
 
 end EuclidGeom

EuclideanGeometry/Foundation/Index.lean

@@ -8,6 +8,8 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Ray
 import EuclideanGeometry.Foundation.Axiom.Linear.Ray_trash
 import EuclideanGeometry.Foundation.Axiom.Linear.Collinear
 import EuclideanGeometry.Foundation.Axiom.Linear.Line
+import EuclideanGeometry.Foundation.Axiom.Linear.Ratio
+import EuclideanGeometry.Foundation.Axiom.Linear.Ratio_trash
 import EuclideanGeometry.Foundation.Axiom.Linear.Class
 import EuclideanGeometry.Foundation.Axiom.Linear.Order
 import EuclideanGeometry.Foundation.Axiom.Linear.Parallel
@@ -28,6 +30,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.Congruence -- `to avoid ambig
 import EuclideanGeometry.Foundation.Axiom.Triangle.Basic_ex
 import EuclideanGeometry.Foundation.Axiom.Triangle.Trigonometric
 import EuclideanGeometry.Foundation.Axiom.Triangle.Similarity
+import EuclideanGeometry.Foundation.Axiom.Triangle.Similarity_trash
 import EuclideanGeometry.Foundation.Axiom.Triangle.IsocelesTriangle
 /- Axiom.Circle -/
 import EuclideanGeometry.Foundation.Axiom.Circle.Basic