diff --git a/EuclideanGeometry/Example/ArefWernick/Chap1.lean b/EuclideanGeometry/Example/ArefWernick/Chap1.lean
index cd478bc7..9157cdd0 100644
--- a/EuclideanGeometry/Example/ArefWernick/Chap1.lean
+++ b/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
diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_1.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_1.lean
index 2d08f096..ca62feee 100644
--- a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_1.lean
+++ b/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⟩
diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_3.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_3.lean
index e4294d45..2107f3aa 100644
--- a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_3.lean
+++ b/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$.
diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_4.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_4.lean
index fc835707..78b8718b 100644
--- a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_4.lean
+++ 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
diff --git a/EuclideanGeometry/Example/ShanZun/Ex1.lean b/EuclideanGeometry/Example/ShanZun/Ex1.lean
index 855c9c9a..d6e6bd49 100644
--- a/EuclideanGeometry/Example/ShanZun/Ex1.lean
+++ b/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$
diff --git a/EuclideanGeometry/Example/ShanZun/Ex1c'.lean b/EuclideanGeometry/Example/ShanZun/Ex1c'.lean
index 8d36d917..f009bbce 100644
--- a/EuclideanGeometry/Example/ShanZun/Ex1c'.lean
+++ b/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
 
diff --git a/EuclideanGeometry/Example/ShanZun/Ex1c.lean b/EuclideanGeometry/Example/ShanZun/Ex1c.lean
index ddf00af0..0a6b3c44 100644
--- a/EuclideanGeometry/Example/ShanZun/Ex1c.lean
+++ b/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,12 +102,12 @@ 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
@@ -115,7 +115,7 @@ lemma hnd'' : ¬ collinear C D E := 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
diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean
index 784a6147..c5d3c058 100644
--- a/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean
+++ b/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
diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean
index 3b8fb79e..3d9b2659 100644
--- a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean
+++ b/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
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean b/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean
index f510b4fb..38fb6dcc 100644
--- a/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean
+++ b/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
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Collinear.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Collinear.lean
index 7c59efc9..c5a84636 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Collinear.lean
+++ b/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. -/
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean
index 972ce606..34c0c489 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean
+++ b/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$. -/
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Ratio.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Ratio.lean
index 4124ba72..1b85569f 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Ratio.lean
+++ b/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
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
index da84aff1..d0b976aa 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
+++ b/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,11 +314,11 @@ 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]
@@ -326,7 +326,7 @@ theorem trivial_of_edge_sum_eq_edge : tr.edge₁.length + tr.edge₂.length = tr
         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
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_trash.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_trash.lean
index 9441e8da..e22765d7 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_trash.lean
+++ b/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
diff --git a/EuclideanGeometry/Foundation/Construction/ComputationTool/Ceva.lean b/EuclideanGeometry/Foundation/Construction/ComputationTool/Ceva.lean
index 19d384a9..9ebcdbd1 100644
--- a/EuclideanGeometry/Foundation/Construction/ComputationTool/Ceva.lean
+++ b/EuclideanGeometry/Foundation/Construction/ComputationTool/Ceva.lean
@@ -49,28 +49,28 @@ attribute [instance] a_ne_b b_ne_c c_ne_a d_ne_a d_ne_b d_ne_c
 --$D,C,A$ are not collinear
 lemma ncolin_dca : ¬ collinear D C A := by
   intro h0
-  exact cad_nd (perm_collinear_snd_trd_fst h0)
+  exact cad_nd (Collinear.perm₂₃₁ h0)
 
 --$E,B,C$ are collinear
 lemma colin_ebc : collinear E B C := by
   have h : E LiesOn LIN C B := by
     rw [e_def]
     apply Line.inx_lies_on_fst
-  exact flip_collinear_fst_trd (Line.pt_pt_linear h)
+  exact Collinear.perm₃₂₁ (Line.pt_pt_linear h)
 
 --$E,D,A$ are collinear
 lemma colin_eda : collinear E D A := by
   have h : E LiesOn LIN A D := by
     rw [e_def]
     apply Line.inx_lies_on_snd
-  exact flip_collinear_fst_trd (Line.pt_pt_linear h)
+  exact Collinear.perm₃₂₁ (Line.pt_pt_linear h)
 
 --$C\ne E$
 instance c_ne_e : PtNe C E := Fact.mk <| by
   have h : collinear E D A := colin_eda
   intro k
   rw [←k] at h
-  exact ncolin_dca (flip_collinear_fst_snd h)
+  exact ncolin_dca (Collinear.perm₂₁₃ h)
 
 --$EB/EC=S_{\trian}DBA/S_{\trian}DCA$
 lemma dratio_ebc_eq_wedge_div_wedge : divratio E B C = (wedge D B A) / (wedge D C A) :=
@@ -79,28 +79,28 @@ lemma dratio_ebc_eq_wedge_div_wedge : divratio E B C = (wedge D B A) / (wedge D
 --$D,A,B$ are not collinear
 lemma ncolin_dab : ¬ collinear D A B := by
   intro h0
-  exact abd_nd (perm_collinear_snd_trd_fst h0)
+  exact abd_nd (Collinear.perm₂₃₁ h0)
 
 --$F,C,A$ are collinear
 lemma colin_fca : collinear F C A := by
   have h : F LiesOn LIN A C := by
     rw [f_def]
     apply Line.inx_lies_on_fst
-  exact flip_collinear_fst_trd (Line.pt_pt_linear h)
+  exact Collinear.perm₃₂₁ (Line.pt_pt_linear h)
 
 --$F,D,B$ are collinear
 lemma colin_fdb : collinear F D B := by
   have h : F LiesOn LIN B D := by
     rw [f_def]
     apply Line.inx_lies_on_snd
-  exact flip_collinear_fst_trd (Line.pt_pt_linear h)
+  exact Collinear.perm₃₂₁ (Line.pt_pt_linear h)
 
 --$A\ne F$
 instance a_ne_f : PtNe A F := Fact.mk <| by
   have h : collinear F D B := colin_fdb
   intro k
   rw [←k] at h
-  exact ncolin_dab (flip_collinear_fst_snd h)
+  exact ncolin_dab (Collinear.perm₂₁₃ h)
 
 --$FC/FA=S_{\trian}DCB/S_{\trian}DAB$
 lemma dratio_fca_eq_wedge_div_wedge : divratio F C A = (wedge D C B) / (wedge D A B) :=
@@ -109,28 +109,28 @@ lemma dratio_fca_eq_wedge_div_wedge : divratio F C A = (wedge D C B) / (wedge D
 --$D,B,C$ are not collinear
 lemma ncolin_dbc : ¬ collinear D B C := by
   intro h0
-  exact bcd_nd (perm_collinear_snd_trd_fst h0)
+  exact bcd_nd (Collinear.perm₂₃₁ h0)
 
 --$G,A,B$ are collinear
 lemma colin_gab : collinear G A B := by
   have h : G LiesOn LIN B A _ := by
     rw [g_def]
     apply Line.inx_lies_on_fst
-  exact flip_collinear_fst_trd (Line.pt_pt_linear h)
+  exact Collinear.perm₃₂₁ (Line.pt_pt_linear h)
 
 --$G,D,C$ are collinear
 lemma colin_gdc : collinear G D C := by
   have h : G LiesOn LIN C D _ := by
     rw [g_def]
     apply Line.inx_lies_on_snd
-  exact flip_collinear_fst_trd (Line.pt_pt_linear h)
+  exact Collinear.perm₃₂₁ (Line.pt_pt_linear h)
 
 --$A\ne F$
 instance b_ne_g : PtNe B G := Fact.mk <| by
   have h : collinear G D C := colin_gdc
   intro k
   rw [←k] at h
-  exact ncolin_dbc (flip_collinear_fst_snd h)
+  exact ncolin_dbc (Collinear.perm₂₁₃ h)
 
 --$GA/GB=S_{\trian}DAC/S_{\trian}DBC$
 lemma dratio_gab_eq_wedge_div_wedge : divratio G A B = (wedge D A C) / (wedge D B C) := ratio_eq_wedge_div_wedge_of_collinear_collinear_notcoliear G A B D C colin_gab colin_gdc ncolin_dbc
diff --git a/EuclideanGeometry/Foundation/Construction/ComputationTool/Oarea_method.lean b/EuclideanGeometry/Foundation/Construction/ComputationTool/Oarea_method.lean
index 510aef68..7fb19afe 100644
--- a/EuclideanGeometry/Foundation/Construction/ComputationTool/Oarea_method.lean
+++ b/EuclideanGeometry/Foundation/Construction/ComputationTool/Oarea_method.lean
@@ -41,7 +41,7 @@ theorem odist_eq_divratio_mul_odist (A B C : P) (dl : DirLine P) (colin : collin
   simp only [map_smul, smul_eq_mul]
 
 theorem  wedge_eq_divratio_mul_wedge_of_collinear_collinear (A B C D E : P) (colin : collinear A B C) [cnea : PtNe C A] (colin' : collinear A D E) : wedge D B E = (divratio A B C) * wedge D C E := by
-  rw[← wedge231 D B E, wedge_eq_wedge_add_wedge_of_collinear E A D B (perm_collinear_trd_fst_snd colin'), ← wedge231 D C E, wedge_eq_wedge_add_wedge_of_collinear E A D C (perm_collinear_trd_fst_snd colin'), wedge213 A B D, wedge231 A B E, wedge213 A C D, wedge231 A C E,wedge_eq_divratio_mul_wedge_of_collinear A B C D colin,wedge_eq_divratio_mul_wedge_of_collinear A B C E colin]
+  rw[← wedge231 D B E, wedge_eq_wedge_add_wedge_of_collinear E A D B (Collinear.perm₃₁₂ colin'), ← wedge231 D C E, wedge_eq_wedge_add_wedge_of_collinear E A D C (Collinear.perm₃₁₂ colin'), wedge213 A B D, wedge231 A B E, wedge213 A C D, wedge231 A C E,wedge_eq_divratio_mul_wedge_of_collinear A B C D colin,wedge_eq_divratio_mul_wedge_of_collinear A B C E colin]
   ring
 
 theorem ratio_eq_wedge_div_wedge_of_collinear_collinear_notcoliear (A B C D E : P) (colin : collinear A B C) [cnea : PtNe C A] (colin' : collinear A D E) (ncolin : ¬ collinear D C E) : divratio A B C = (wedge D B E) / (wedge D C E) := by
diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_old.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_old.lean
index 80b375ac..dfdae19e 100644
--- a/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_old.lean
+++ b/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_old.lean
@@ -184,7 +184,7 @@ theorem Parallelogram_not_collinear₁₂₃ (P : Type*) [EuclideanPlane P] (qdr
          simp only [neg_smul, one_smul, neg_vec]
          rw[o]
        exact collinear_of_vec_eq_smul_vec' ooo
-     simp only [flip_collinear_fst_snd oo, not_true_eq_false] at h
+     simp only [Collinear.perm₂₁₃ oo, not_true_eq_false] at h
    have hcd : qdr_nd.point₃ ≠ qdr_nd.point₄ := by
      by_contra k₂
      have k₂₂ : VEC qdr_nd.point₄ qdr_nd.point₃=0 := by
@@ -196,7 +196,7 @@ theorem Parallelogram_not_collinear₁₂₃ (P : Type*) [EuclideanPlane P] (qdr
      simp only [k₂₃.symm, ne_eq, not_true_eq_false] at hba
    have t : ¬ collinear qdr_nd.point₂ qdr_nd.point₁ qdr_nd.point₃ := by
      by_contra k
-     simp only [flip_collinear_fst_snd k, not_true_eq_false] at h
+     simp only [Collinear.perm₂₁₃ k, not_true_eq_false] at h
    have x : ¬ collinear_of_nd (A := qdr_nd.point₂) (B := qdr_nd.point₁) (C := qdr_nd.point₃) := by
      unfold collinear at t
      simp only [hca, hbc, hba.symm, or_self, dite_false] at t
@@ -287,7 +287,7 @@ theorem Parallelogram_not_collinear₁₂₃ (P : Type*) [EuclideanPlane P] (qdr
        rw[l₂',l₃]
        exact k₁
      simp[p₄] at s₂
-   simp [flip_collinear_fst_snd m₃] at m₂
+   simp [Collinear.perm₂₁₃ m₃] at m₂
    by_contra m₅
    have m₄ :  ¬ collinear qdr_nd.point₄ qdr_nd.point₃ qdr_nd.point₁ := by
      by_contra k₂
@@ -298,7 +298,7 @@ theorem Parallelogram_not_collinear₁₂₃ (P : Type*) [EuclideanPlane P] (qdr
        rw[l₄',l₃']
        exact k₂
      simp[p₅] at s₃
-   simp [flip_collinear_fst_snd m₅] at m₄
+   simp [Collinear.perm₂₁₃ m₅] at m₄
    by_contra m₇
    have m₆ :  ¬ collinear qdr_nd.point₁ qdr_nd.point₄ qdr_nd.point₂ := by
      by_contra k₃
@@ -309,7 +309,7 @@ theorem Parallelogram_not_collinear₁₂₃ (P : Type*) [EuclideanPlane P] (qdr
        rw[l₄,l₁]
        exact k₃
      simp [p₆] at s₄
-   simp [flip_collinear_fst_snd m₇] at m₆
+   simp [Collinear.perm₂₁₃ m₇] at m₆
 
 /-- If qdr_nd is non-degenerate and is a parallelogram, and its 2nd, 3rd and 4th points are not collinear, then qdr_nd is a parallelogram_nd.-/
 theorem Parallelogram_not_collinear₂₃₄ (P : Type*) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) (para: qdr_nd.1 IsParallelogram) (h: ¬ collinear qdr_nd.point₂ qdr_nd.point₃ qdr_nd.point₄) : qdr_nd IsParallelogram_nd := by
@@ -492,12 +492,12 @@ theorem qdr_nd_is_prg_nd_of_para_para_not_collinear₁₂₃ (h₁ : qdr_nd.edge
     rw [(smul_smul (- r) c (VEC qdr_nd.point₁ qdr_nd.point₂)).symm,eq''.symm,neg_smul,eq.symm]
     exact (neg_vec qdr_nd.point₃ qdr_nd.point₁).symm
   by_contra iscollinear
-  apply flip_collinear_fst_trd at iscollinear
+  apply Collinear.perm₃₂₁ at iscollinear
   rw [collinear_iff_eq_smul_vec_of_ne] at iscollinear
   rcases iscollinear with ⟨r,eq⟩
   apply notcollinear
   have para : qdr_nd.edge_nd₃₄.toVecND ∥ qdr_nd.edge_nd₁₂.toVecND := by sorry
-  apply flip_collinear_fst_trd
+  apply Collinear.perm₃₂₁
   rw [collinear_iff_eq_smul_vec_of_ne]
   rcases (para_vec qdr_nd.edge_nd₃₄.toVecND qdr_nd.edge_nd₁₂.toVecND para) with ⟨c,eq'⟩
   have eq'' : (VEC qdr_nd.point₃ qdr_nd.point₄) = c • (VEC qdr_nd.point₁ qdr_nd.point₂) := eq'
diff --git a/EuclideanGeometry/Foundation/Tactic/Collinear/perm_collinear.lean b/EuclideanGeometry/Foundation/Tactic/Collinear/perm_collinear.lean
index f56b1d05..4a29c85e 100644
--- a/EuclideanGeometry/Foundation/Tactic/Collinear/perm_collinear.lean
+++ b/EuclideanGeometry/Foundation/Tactic/Collinear/perm_collinear.lean
@@ -35,31 +35,31 @@ def evalPerm_collinear : Tactic := fun stx =>
       catch
         _ => pure ()
       try
-        let t <- `(tactic| refine flip_collinear_fst_snd $x0)
+        let t <- `(tactic| refine Collinear.perm₂₁₃ $x0)
         evalTactic t
         return
       catch
         _ => pure ()
       try
-        let t <- `(tactic| refine flip_collinear_snd_trd $x0)
+        let t <- `(tactic| refine Collinear.perm₁₃₂ $x0)
         evalTactic t
         return
       catch
         _ => pure ()
       try
-        let t <- `(tactic| refine flip_collinear_fst_snd (flip_collinear_snd_trd $x0))
+        let t <- `(tactic| refine Collinear.perm₂₁₃ (Collinear.perm₁₃₂ $x0))
         evalTactic t
         return
       catch
         _ => pure ()
       try
-        let t <- `(tactic| refine flip_collinear_snd_trd (flip_collinear_fst_snd $x0))
+        let t <- `(tactic| refine Collinear.perm₁₃₂ (Collinear.perm₂₁₃ $x0))
         evalTactic t
         return
       catch
         _ => pure ()
       try
-        let t <- `(tactic| refine flip_collinear_fst_snd (flip_collinear_snd_trd (flip_collinear_fst_snd $x0)))
+        let t <- `(tactic| refine Collinear.perm₂₁₃ (Collinear.perm₁₃₂ (Collinear.perm₂₁₃ $x0)))
         evalTactic t
         return
       catch
diff --git a/EuclideanGeometry/Unused/Line.lean b/EuclideanGeometry/Unused/Line.lean
index a299f4c0..c629165b 100644
--- a/EuclideanGeometry/Unused/Line.lean
+++ b/EuclideanGeometry/Unused/Line.lean
@@ -39,10 +39,10 @@ def mk_pt_pt (A B : P) (h : B ≠ A) : Line P where
         exact triv_collinear _ _
       · by_cases tz = tx
         · rw [pt_eq_pt_of_eq_smul_smul h hz hx]
-          exact flip_collinear_snd_trd $ triv_collinear _ _
+          exact Collinear.perm₁₃₂ $ triv_collinear _ _
         · have h : ty = tz := by tauto
           rw [pt_eq_pt_of_eq_smul_smul h hy hz]
-          exact flip_collinear_fst_snd $ flip_collinear_snd_trd $ triv_collinear _ _
+          exact Collinear.perm₂₁₃ $ Collinear.perm₁₃₂ $ triv_collinear _ _
   maximal x y := by
     unfold Membership.mem Set.instMembershipSet Set.Mem setOf
     simp only [forall_exists_index]
diff --git a/Plan_files/DetailedPlan/Axiom-Linear.txt b/Plan_files/DetailedPlan/Axiom-Linear.txt
index 6a3481e7..1e4fc298 100644
--- a/Plan_files/DetailedPlan/Axiom-Linear.txt
+++ b/Plan_files/DetailedPlan/Axiom-Linear.txt
@@ -366,10 +366,10 @@ Theorem \verb|collinear_iff_eq_smul_vec_of_ne|: Given three points $A$, $B$, $C$
 Theorem \verb|triv_collinear|: For any two points $A$ and $C$, the points $A$, $A$, $C$ are collinear.
 
 \item 
-Theorem \verb|flip_collinear_snd_trd|: 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 \verb|Collinear.perm₁₃₂|: 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.
 
 \item 
-Theorem \verb|flip_collinear_fst_snd|: 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 \verb|Collinear.perm₂₁₃|: 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.
 
 \item 
 Theorem \verb|collinear_of_collinear_collinear_ne|: 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.