fix

EuclideanGeometry/Example/ArefWernick/Chap1.lean

@@ -61,7 +61,7 @@ lemma B_ne_f : B ≠ F := by
       exact ⟨(SegND B C (ne_of_not_collinear hnd).1).source_lies_on_toLine , (SegND A B (ne_of_not_collinear hnd).2.2).target_lies_on_toLine ⟩
     exact d_ne_b (unique_of_inx_of_line_of_not_para line_neq inxb.symm inxd.symm)
   have bcd_notcoli : ¬ collinear B C D := (Line.lies_on_line_of_pt_pt_iff_collinear (b_ne_c (hnd := hnd)).symm D).mpr.mt d_not_lies_on_bc
-  have b_not_lies_on_cd : ¬ B LiesOn (LIN C D d_ne_c) := (Line.lies_on_line_of_pt_pt_iff_collinear d_ne_c B).mp.mt (flip_collinear_snd_trd.mt (flip_collinear_fst_snd.mt bcd_notcoli))
+  have b_not_lies_on_cd : ¬ B LiesOn (LIN C D d_ne_c) := (Line.lies_on_line_of_pt_pt_iff_collinear d_ne_c B).mp.mt (Collinear.perm₁₃₂.mt (Collinear.perm₂₁₃.mt bcd_notcoli))
   have f_lies_on_seg_cd : F LiesOn (SegND C D d_ne_c).1 := hf.2
   exact (ne_of_lieson_and_not_lieson (SegND.lies_on_toLine_of_lie_on f_lies_on_seg_cd) b_not_lies_on_cd).symm
 lemma d_ne_f : D ≠ F := sorry

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_1.lean

@@ -35,10 +35,10 @@ structure Setting1  (Plane : Type*) [EuclideanPlane Plane] where
   h₂ : (SEG B C).length = (SEG D E).length
 attribute [instance] Setting1.B_ne_F
 lemma hnd₁ {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: ¬ collinear e.B e.A e.C := by
-  apply flip_collinear_fst_snd.mt
+  apply Collinear.perm₂₁₃.mt
   exact e.ABC_nd
 lemma hnd₂ {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: ¬ collinear e.D e.F e.E := by
-  apply perm_collinear_trd_fst_snd.mt
+  apply Collinear.perm₃₁₂.mt
   exact e.EDF_nd
 instance A_ne_B {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.A e.B := ⟨(ne_of_not_collinear hnd₁).2.2⟩
 instance D_ne_E {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.D e.E := ⟨(ne_of_not_collinear hnd₂).2.1⟩

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_3.lean

@@ -38,7 +38,7 @@ theorem Result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : ∠
   have h₂ : ¬ collinear e.D e.B e.C := by
     have h₂' : ¬ collinear e.B e.D e.C := by
       exact (Quadrilateral_cvx.not_collinear₂₃₄ (QDR_cvx e.A e.B e.D e.C e.cvx_ABDC))
-    apply flip_collinear_fst_snd.mt h₂'
+    apply Collinear.perm₂₁₃.mt h₂'
   have C_ne_B : e.C ≠ e.B := by
     exact (Quadrilateral_cvx.nd₂₄ (QDR_cvx e.A e.B e.D e.C e.cvx_ABDC))
   --Because $AB = AC$ ,we have $\angle A B C = -\angle A C B$.

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_4.lean

@@ -53,7 +53,7 @@ theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : ∠
   Thus $\angle B D E = -\angle C B A $.
   -/
   have hnd₁' : ¬ collinear e.C e.A e.B := by
-    apply perm_collinear_trd_fst_snd.mt
+    apply Collinear.perm₃₁₂.mt
     exact e.hnd₁
   --$DB = BC$
   have e₂ : (SEG e.D e.B).length = (SEG e.B e.C).length := by

EuclideanGeometry/Example/ShanZun/Ex1.lean

@@ -59,7 +59,7 @@ lemma B_ne_C : B ≠ C := (ne_of_not_collinear hnd).1.symm
 variable {D E : P} {hd : D LiesInt (SEG_nd A B (B_ne_a (hnd := hnd))).extension} {he : E LiesInt (SEG_nd A C (c_ne_a (hnd := hnd))).extension}
 -- Claim: $E \ne B$ and $D \ne C$. This is because $E$ lies on line $AC$, but $B$ doesn't lies on $AC$; $D$ lies on line $AB$, but $C$ doesn't lies on $AB$.
 lemma e_ne_B : E ≠ B := by -- for $E \ne B$
-  have b_not_lieson_ac := (Line.lies_on_line_of_pt_pt_iff_collinear (_h := ⟨ c_ne_a (hnd := hnd)⟩) B).mp.mt (flip_collinear_snd_trd.mt hnd) -- $B$ doesn't lies on line $AC$ because $A, B, C$ not collinear
+  have b_not_lieson_ac := (Line.lies_on_line_of_pt_pt_iff_collinear (_h := ⟨ c_ne_a (hnd := hnd)⟩) B).mp.mt (Collinear.perm₁₃₂.mt hnd) -- $B$ doesn't lies on line $AC$ because $A, B, C$ not collinear
   have e_lieson_ac := SegND.lies_on_toLine_of_lies_on_extn (Ray.lies_on_of_lies_int he) -- $E$ lieson line $AC$ because $E$ lies in the extension of $AC$
   exact ne_of_lieson_and_not_lieson e_lieson_ac b_not_lieson_ac -- $E \ne B$ because $E$ lies on line $AC$, but $B$ doesn't lies on line $AC$
 lemma d_ne_c : D ≠ C := by -- for $D \ne C$

EuclideanGeometry/Example/ShanZun/Ex1c'.lean

@@ -93,21 +93,21 @@ theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : (SEG
     have : collinear e.A e.B E := by
       apply collinear_of_collinear_collinear_ne adb_collinear h' D_ne_A
     have neghnd : collinear e.A e.B e.C := by
-      apply collinear_of_collinear_collinear_ne (flip_collinear_snd_trd this) aec_collinear E_ne_A
+      apply collinear_of_collinear_collinear_ne (Collinear.perm₁₃₂ this) aec_collinear E_ne_A
     exact e.not_collinear_ABC neghnd
   have not_collinear_CDE : ¬ collinear e.C e.D E := by
     intro h
     have : collinear e.C e.D e.A := by
-      apply flip_collinear_snd_trd
+      apply Collinear.perm₁₃₂
       apply collinear_of_collinear_collinear_ne
-      apply (flip_collinear_snd_trd (flip_collinear_fst_snd (flip_collinear_snd_trd aec_collinear)))
-      apply flip_collinear_snd_trd h
+      apply (Collinear.perm₁₃₂ (Collinear.perm₂₁₃ (Collinear.perm₁₃₂ aec_collinear)))
+      apply Collinear.perm₁₃₂ h
       apply E_ne_C
     have : collinear e.A e.B e.C := by
       apply collinear_of_collinear_collinear_ne
       apply adb_collinear
       -- apply e.hD
-      apply (flip_collinear_snd_trd (flip_collinear_fst_snd (flip_collinear_snd_trd this)))
+      apply (Collinear.perm₁₃₂ (Collinear.perm₂₁₃ (Collinear.perm₁₃₂ this)))
       apply D_ne_A
     apply e.not_collinear_ABC this
 

EuclideanGeometry/Example/ShanZun/Ex1c.lean

@@ -29,7 +29,7 @@ lemma d_ne_a: D ≠ A := by
   use C
   by_contra h
   have : collinear A B C :=by
-    apply flip_collinear_fst_snd h
+    apply Collinear.perm₂₁₃ h
   trivial
 --Introduce the midpoint E of AC
 variable {E : P} {he : E=  (SEG A C).midpoint}
@@ -92,7 +92,7 @@ lemma hnd': ¬ collinear A D E := by
     exact hnd
     exact hd
   have neghnd : collinear A B C := by
-    apply collinear_of_collinear_collinear_ne (flip_collinear_snd_trd this) aec_collinear e_ne_a
+    apply collinear_of_collinear_collinear_ne (Collinear.perm₁₃₂ this) aec_collinear e_ne_a
     exact he
     use B
     use C
@@ -102,20 +102,20 @@ lemma hnd': ¬ collinear A D E := by
 lemma hnd'' : ¬ collinear C D E := by
   intro h
   have : collinear C D A := by
-    apply flip_collinear_snd_trd
+    apply Collinear.perm₁₃₂
     apply collinear_of_collinear_collinear_ne
-    apply (flip_collinear_snd_trd (flip_collinear_fst_snd (flip_collinear_snd_trd aec_collinear)))
+    apply (Collinear.perm₁₃₂ (Collinear.perm₂₁₃ (Collinear.perm₁₃₂ aec_collinear)))
     use E
     exact he
-    apply flip_collinear_snd_trd h
+    apply Collinear.perm₁₃₂ h
     apply e_ne_C
     apply hnd
     exact he
   have : collinear A B C := by
     apply collinear_of_collinear_collinear_ne
     apply adb_collinear
     apply hd
-    apply (flip_collinear_snd_trd (flip_collinear_fst_snd (flip_collinear_snd_trd this)))
+    apply (Collinear.perm₁₃₂ (Collinear.perm₂₁₃ (Collinear.perm₁₃₂ this)))
     apply d_ne_a
     apply hnd
     exact hd

EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean

@@ -183,7 +183,7 @@ lemma pts_lieson_circle_vec_eq {A B : P} {ω : Circle P} [hne : PtNe B A] (hl₁
   apply vec_eq_dist_eq_of_lies_on_line_pt_pt_of_ptNe
   · have : (perp_foot ω.center (LIN A B)) LiesOn (LIN A B) := perp_foot_lies_on_line _ _
     have : collinear A B (perp_foot ω.center (LIN A B)) := Line.pt_pt_linear this
-    have : collinear (perp_foot ω.center (LIN A B)) A B := perm_collinear_trd_fst_snd this
+    have : collinear (perp_foot ω.center (LIN A B)) A B := Collinear.perm₃₁₂ this
     apply Line.pt_pt_maximal this
   apply (sq_eq_sq dist_nonneg dist_nonneg).mp
   calc

EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean

@@ -115,7 +115,7 @@ theorem extangent_pt_centers_collinear {ω₁ : Circle P} {ω₂ : Circle P} (h
         simp
       _ = ω₁.radius • (‖VEC ω₁.center ω₂.center‖⁻¹ • (VEC ω₁.center ω₂.center)) := rfl
       _ = (ω₁.radius * ‖VEC ω₁.center ω₂.center‖⁻¹) • (VEC ω₁.center ω₂.center) := by apply smul_smul
-  apply flip_collinear_snd_trd (collinear_of_vec_eq_smul_vec this)
+  apply Collinear.perm₁₃₂ (collinear_of_vec_eq_smul_vec this)
 
 end CC
 

EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean

@@ -161,7 +161,7 @@ theorem antipode_iff_collinear (A B : P) {ω : Circle P} [h : PtNe B A] (h₁ :
 
 theorem mk_pt_pt_diam_isantipode {A B : P} [h : PtNe A B] : Arc.IsAntipode A B (Circle.mk_pt_pt_diam_fst_lieson) (Circle.mk_pt_pt_diam_snd_lieson) := by
   have hc : collinear (SEG A B).midpoint A B := by
-    apply perm_collinear_trd_fst_snd
+    apply Collinear.perm₃₁₂
     apply Line.pt_pt_linear
     show (SEG A B).midpoint LiesOn (SEG_nd A B).toLine
     apply SegND.lies_on_toLine_of_lie_on

EuclideanGeometry/Foundation/Axiom/Linear/Collinear.lean

@@ -89,7 +89,7 @@ theorem collinear_of_snd_eq_fst {A B : P} (C : P) (h : B = A)  : collinear A B C
   (dite_prop_iff_or (C = B ∨ A = C ∨ B = A)).mpr (.inl ⟨.inr (.inr h), trivial⟩)
 
 /-- Given three points $A$, $B$, and $C$, if $A$, $B$, $C$ are collinear (in that order), then $A$, $C$, $B$ are collinear (in that order); in other words, swapping the last two of the three points does not change the definition of colinarity. -/
-theorem flip_collinear_snd_trd {A B C : P} (c : collinear A B C) : collinear A C B := by
+theorem Collinear.perm₁₃₂ {A B C : P} (c : collinear A B C) : collinear A C B := by
   by_cases h : B ≠ A ∧ C ≠ A
   · haveI : PtNe B A := ⟨h.1⟩
     rcases collinear_iff_eq_smul_vec_of_ne.1 c with ⟨t, e⟩
@@ -108,7 +108,7 @@ theorem flip_collinear_snd_trd {A B C : P} (c : collinear A B C) : collinear A C
     exact g.2.2 $ h g.2.1.symm
 
 /-- Given three points $A$, $B$, and $C$, if $A$, $B$, $C$ are collinear (in that order), then $B$, $A$, $C$ are collinear (in that order); in other words, in the definition of colinarity, swapping the first two of the three points does not change property of the three points being collinear. -/
-theorem flip_collinear_fst_snd {A B C : P} (c : collinear A B C) : collinear B A C := by
+theorem Collinear.perm₂₁₃ {A B C : P} (c : collinear A B C) : collinear B A C := by
   by_cases h : B = A
   · rw [h]
     exact triv_collinear _ _
@@ -119,14 +119,14 @@ theorem flip_collinear_fst_snd {A B C : P} (c : collinear A B C) : collinear B A
       rw [← vec_sub_vec A B C, e, ← neg_vec A B, smul_neg, sub_smul, neg_sub, one_smul]
     exact collinear_of_vec_eq_smul_vec e'
 
-theorem perm_collinear_snd_trd_fst {A B C : P} (h : collinear A B C) : collinear B C A :=
-  flip_collinear_snd_trd (flip_collinear_fst_snd h)
+theorem Collinear.perm₂₃₁ {A B C : P} (h : collinear A B C) : collinear B C A :=
+  Collinear.perm₁₃₂ (Collinear.perm₂₁₃ h)
 
-theorem perm_collinear_trd_fst_snd {A B C : P} (h : collinear A B C) : collinear C A B :=
-  perm_collinear_snd_trd_fst (perm_collinear_snd_trd_fst h)
+theorem Collinear.perm₃₁₂ {A B C : P} (h : collinear A B C) : collinear C A B :=
+  Collinear.perm₂₃₁ (Collinear.perm₂₃₁ h)
 
-theorem flip_collinear_fst_trd {A B C : P} (h : collinear A B C) : collinear C B A :=
-  perm_collinear_snd_trd_fst (flip_collinear_snd_trd h)
+theorem Collinear.perm₃₂₁ {A B C : P} (h : collinear A B C) : collinear C B A :=
+  Collinear.perm₂₃₁ (Collinear.perm₁₃₂ h)
 
 -- the proof of this theorem using def of line seems to be easier
 /-- Given four points $A$, $B$, $C$, $D$ with $B \neq A$, if $A$, $B$, $C$ are collinear, and if $A$, $B$, $D$ are collinear, then $A$, $C$, $D$ are collinear. -/

EuclideanGeometry/Foundation/Axiom/Linear/Line.lean

@@ -1031,7 +1031,7 @@ theorem pt_pt_linear {A B C : P} [_h : PtNe B A] (hc : C LiesOn (LIN A B)) : col
   if hcb : C = B then collinear_of_trd_eq_snd A hcb
   else if hac : A = C then collinear_of_fst_eq_snd B hac
   else haveI : PtNe C B := ⟨hcb⟩
-  perm_collinear_trd_fst_snd <| (dite_prop_iff_or _).mpr <| .inr ⟨by push_neg; exact ⟨hac, Fact.out, hcb⟩,
+  Collinear.perm₃₁₂ <| (dite_prop_iff_or _).mpr <| .inr ⟨by push_neg; exact ⟨hac, Fact.out, hcb⟩,
     ((lies_on_iff_eq_toProj_of_lies_on snd_pt_lies_on_mk_pt_pt).mp hc).trans <|
       congrArg toProj line_of_pt_pt_eq_rev⟩
 
@@ -1051,7 +1051,7 @@ theorem pt_pt_maximal {A B C : P} [_h : PtNe B A] (Co : collinear A B C) : C Lie
     exact snd_pt_lies_on_mk_pt_pt
   else haveI : PtNe C B := ⟨hcb⟩
   (lies_on_iff_eq_toProj_of_lies_on snd_pt_lies_on_mk_pt_pt).mpr <|
-    (collinear_iff_toProj_eq_of_ptNe.mp (perm_collinear_snd_trd_fst Co)).trans <|
+    (collinear_iff_toProj_eq_of_ptNe.mp (Collinear.perm₂₃₁ Co)).trans <|
       congrArg Line.toProj (line_of_pt_pt_eq_rev (_h := _h)).symm
 
 /-- Given two distinct points $A$ and $B$ on a line $l$, if a point $C$ is so that $A$, $B$, and $C$ are collinear, then $C$ lines on $l$. -/

EuclideanGeometry/Foundation/Axiom/Linear/Ratio.lean

@@ -12,13 +12,13 @@ section ratio
 /-
 Below is the definition of divratio using ddist, which I think might not be a good idea.
 
-def divratio (A B C : P) (colin : collinear A B C) (cnea : C ≠ A) : ℝ := (DirLine.ddist (B := B) (DirLine.pt_pt_maximal cnea (flip_collinear_snd_trd (triv_collinear A C))) (DirLine.pt_pt_maximal cnea (flip_collinear_snd_trd colin))) / (DirLine.ddist (DirLine.pt_pt_maximal cnea (flip_collinear_snd_trd (triv_collinear A C))) (DirLine.pt_pt_maximal cnea (perm_collinear_trd_fst_snd (triv_collinear C A))))
+def divratio (A B C : P) (colin : collinear A B C) (cnea : C ≠ A) : ℝ := (DirLine.ddist (B := B) (DirLine.pt_pt_maximal cnea (Collinear.perm₁₃₂ (triv_collinear A C))) (DirLine.pt_pt_maximal cnea (Collinear.perm₁₃₂ colin))) / (DirLine.ddist (DirLine.pt_pt_maximal cnea (Collinear.perm₁₃₂ (triv_collinear A C))) (DirLine.pt_pt_maximal cnea (Collinear.perm₃₁₂ (triv_collinear C A))))
 -/
 
 def divratio (A B C : P) : ℝ := ((VEC A B)/(VEC A C)).1
 
 theorem ratio_is_real' (A B C : P) (colin : collinear A B C) [cnea : PtNe C A] : ((VEC A B)/(VEC A C)).2 = 0 := by
-  have h0 : collinear A C B := flip_collinear_snd_trd colin
+  have h0 : collinear A C B := Collinear.perm₁₃₂ colin
   rw [collinear_iff_eq_smul_vec_of_ne] at h0
   rcases h0 with ⟨r , h1⟩
   have h2 : VEC A C ≠ 0 := (ne_iff_vec_ne_zero A C).mp cnea.out
@@ -73,7 +73,7 @@ theorem pt_eq_of_ratio_eq_of_ne_ne (A B C D : P) [cned : PtNe C D] [dnea : PtNe
   have h0 : divratio C A D = divratio C B D := by
     rw [ratio_eq_ratio_div_ratio_minus_one A C D colinacd, req, ratio_eq_ratio_div_ratio_minus_one B C D colinbcd]
   have h1 : VEC C A = VEC C B := by
-    rw [vec_eq_vec_smul_ratio C A D (flip_collinear_fst_snd colinacd), vec_eq_vec_smul_ratio C B D (flip_collinear_fst_snd colinbcd), h0]
+    rw [vec_eq_vec_smul_ratio C A D (Collinear.perm₂₁₃ colinacd), vec_eq_vec_smul_ratio C B D (Collinear.perm₂₁₃ colinbcd), h0]
   rw [← start_vadd_vec_eq_end C A, h1, start_vadd_vec_eq_end C B]
 
 theorem ratio_eq_zero_of_point_eq1 (A B : P) : divratio A A B = 0 := by

EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean

@@ -192,9 +192,9 @@ end Triangle
 
 namespace TriangleND
 
-def perm_vertices : (TriangleND P) := ⟨tr_nd.1.perm_vertices, flip_collinear_snd_trd.mt $ flip_collinear_fst_snd.mt tr_nd.2⟩
+def perm_vertices : (TriangleND P) := ⟨tr_nd.1.perm_vertices, Collinear.perm₁₃₂.mt $ Collinear.perm₂₁₃.mt tr_nd.2⟩
 
-def flip_vertices : (TriangleND P) := ⟨tr_nd.1.flip_vertices, flip_collinear_snd_trd.mt tr_nd.2⟩
+def flip_vertices : (TriangleND P) := ⟨tr_nd.1.flip_vertices, Collinear.perm₁₃₂.mt tr_nd.2⟩
 
 theorem eq_self_of_perm_vertices_three_times : tr_nd.perm_vertices.perm_vertices.perm_vertices = tr_nd := rfl
   --exact tr_nd.1.eq_self_of_perm_vertices_three_times
@@ -314,19 +314,19 @@ theorem trivial_of_edge_sum_eq_edge : tr.edge₁.length + tr.edge₂.length = tr
   rw [not_not]
   by_cases h₁ : VEC B C = 0
   · simp only [(eq_iff_vec_eq_zero B C).2 h₁]
-    apply flip_collinear_fst_trd
+    apply Collinear.perm₃₂₁
     exact triv_collinear _ _
   · by_cases h₂ : VEC C A = 0
     · simp only [(eq_iff_vec_eq_zero C A).2 h₂]
-      apply flip_collinear_snd_trd
+      apply Collinear.perm₁₃₂
       exact triv_collinear _ _
     · have g : SameRay ℝ (VEC B C) (VEC C A)
       · rw [sameRay_iff_norm_add, ← eq]
         congr <;>
         exact Seg.length_eq_norm_toVec
       rcases SameRay.exists_pos g h₁ h₂ with ⟨_, ⟨_, ⟨_, ⟨_, g⟩⟩⟩⟩
       rw [← neg_vec C B, ← neg_one_smul ℝ, ← mul_smul, mul_neg_one, ← eq_inv_smul_iff₀ (by linarith), ← mul_smul] at g
-      exact perm_collinear_snd_trd_fst (collinear_of_vec_eq_smul_vec g)
+      exact Collinear.perm₂₃₁ (collinear_of_vec_eq_smul_vec g)
 
 theorem triangle_ineq' (nontriv : tr.IsND) : tr.edge₁.length + tr.edge₂.length > tr.edge₃.length := by
   have ne : tr.edge₁.length + tr.edge₂.length ≠ tr.edge₃.length := by

EuclideanGeometry/Foundation/Axiom/Triangle/Basic_trash.lean

@@ -22,7 +22,7 @@ theorem edge_toLine_not_para_of_not_collinear {A B C : P} (h : ¬ collinear A B
     exact (SEG_nd B C (ne_of_not_collinear h).1).source_lies_on_toLine
     exact h1
   have a_lies_on_ab : A LiesOn (LIN A B (ne_of_not_collinear h).2.2) := (SEG_nd A B (ne_of_not_collinear h).2.2).source_lies_on_toLine
-  have a_not_lies_on_bc := (Line.lies_on_line_of_pt_pt_iff_collinear (_h := ⟨(ne_of_not_collinear h).1⟩) A).mp.mt (flip_collinear_snd_trd.mt (flip_collinear_fst_snd.mt h))
+  have a_not_lies_on_bc := (Line.lies_on_line_of_pt_pt_iff_collinear (_h := ⟨(ne_of_not_collinear h).1⟩) A).mp.mt (Collinear.perm₁₃₂.mt (Collinear.perm₂₁₃.mt h))
   simp only[← eq1] at a_not_lies_on_bc
   apply a_not_lies_on_bc
   exact a_lies_on_ab
@@ -34,7 +34,7 @@ theorem edge_toLine_not_para_of_not_collinear {A B C : P} (h : ¬ collinear A B
     exact (SEG_nd C A (ne_of_not_collinear h).2.1).source_lies_on_toLine
     exact h2
   have b_lies_on_bc : B LiesOn (LIN B C (ne_of_not_collinear h).1) := (SEG_nd B C (ne_of_not_collinear h).1).source_lies_on_toLine
-  have b_not_lies_on_ca := (Line.lies_on_line_of_pt_pt_iff_collinear (_h := ⟨(ne_of_not_collinear h).2.1⟩) B).mp.mt (flip_collinear_fst_snd.mt (flip_collinear_snd_trd.mt h))
+  have b_not_lies_on_ca := (Line.lies_on_line_of_pt_pt_iff_collinear (_h := ⟨(ne_of_not_collinear h).2.1⟩) B).mp.mt (Collinear.perm₂₁₃.mt (Collinear.perm₁₃₂.mt h))
   simp only[← eq2] at b_not_lies_on_ca
   apply b_not_lies_on_ca
   exact b_lies_on_bc