From 3bb29610f48bd9c2c1bb25edd59d77b9dbd995eb Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Fri, 12 Jan 2024 13:51:15 +0800
Subject: [PATCH 1/6] Refine Orientation_trash

---
 .../Axiom/Position/Orientation_trash.lean      | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean b/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean
index 3701c44c..149a8a4f 100644
--- a/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean
@@ -47,18 +47,28 @@ theorem eq_toDir_of_parallel_and_same_side {A B C D : P} {h : A ≠ B} {h₁ : C
   have Proj : (SEG_nd A C h₁).toProj = (SEG_nd B D h₂).toProj := by
     exact para
   have eq_or_neg : ((SEG_nd A C h₁).toDir = (SEG_nd B D h₂).toDir) ∨ ((SEG_nd A C h₁).toDir = -(SEG_nd B D h₂).toDir) := by
-    sorry
+    apply Dir.toProj_eq_toProj_iff.mp
+    exact Proj
   rcases eq_or_neg with eq|neg
   · exact eq
-  · sorry
+  · have : C LiesOnLeft (SEG_nd A B h.symm) ∧ D LiesOnLeft (SEG_nd A B h.symm) ∨ C LiesOnRight (SEG_nd A B h.symm) ∧ D LiesOnRight (SEG_nd A B h.symm) := by
+      exact side
+    rcases this with ll|rr
+    · sorry
+    · sorry
 --Guan Nailin
 theorem neg_toDir_of_parallel_and_opposite_side {A B C D : P} {h : A ≠ B} {h₁ : C ≠ A} {h₂ : D ≠ B} {para : (SEG_nd A C h₁) ∥ (SEG_nd B D h₂)} {side : IsOnOppositeSide C D (SEG_nd A B h.symm)} : (SEG_nd A C h₁).toDir = -(SEG_nd B D h₂).toDir := by
   have Proj : (SEG_nd A C h₁).toProj = (SEG_nd B D h₂).toProj := by
     exact para
   have eq_or_neg : ((SEG_nd A C h₁).toDir = (SEG_nd B D h₂).toDir) ∨ ((SEG_nd A C h₁).toDir = -(SEG_nd B D h₂).toDir) := by
-    sorry
+    apply Dir.toProj_eq_toProj_iff.mp
+    exact Proj
   rcases eq_or_neg with eq|neg
-  · sorry
+  · have : C LiesOnLeft (SEG_nd A B h.symm) ∧ D LiesOnRight (SEG_nd A B h.symm) ∨ C LiesOnRight (SEG_nd A B h.symm) ∧ D LiesOnLeft (SEG_nd A B h.symm) := by
+      exact side
+    rcases this with lr|rl
+    · sorry
+    · sorry
   · exact neg
 
 end EuclidGeom

From 9a7a9b832c8d9b1f8235cf3b3a187436698e546b Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Fri, 12 Jan 2024 18:00:50 +0800
Subject: [PATCH 2/6] 1.12

---
 .../Foundation/Axiom/Basic/Angle.lean         |  4 +++-
 .../Foundation/Axiom/Basic/Vector.lean        |  6 ++---
 .../Foundation/Axiom/Circle/CCPosition.lean   |  2 --
 .../Axiom/Position/Orientation_trash.lean     | 23 ++++++++++++++++++-
 4 files changed, 28 insertions(+), 7 deletions(-)

diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Angle.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Angle.lean
index 8510ec7a..a25b517a 100644
--- a/EuclideanGeometry/Foundation/Axiom/Basic/Angle.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Basic/Angle.lean
@@ -1,5 +1,5 @@
 import EuclideanGeometry.Foundation.Axiom.Basic.Angle.AddToMathlib
-
+import Mathlib.Data.Int.Parity
 /-!
 # Angle Conversions
 
@@ -16,6 +16,8 @@ In this file, we define suitable coversion function between `ℝ⧸2π`,`ℝ⧸
 
 noncomputable section
 
+attribute [ext] Complex.ext
+
 namespace EuclidGeom
 
 open AngValue Classical Real
diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
index 6a4166f0..c6612977 100644
--- a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
@@ -184,7 +184,7 @@ lemma toComplex_inv (z : 𝕜) : ↑(z⁻¹) = (z : ℂ)⁻¹ := by ext <;> simp
 
 @[simp, norm_cast]
 lemma abs_toComplex (z : 𝕜) : Complex.abs (z : ℂ) = ‖z‖ := by
-  rw [← pow_left_inj (map_nonneg _ _) (norm_nonneg _) zero_lt_two,
+  rw [← pow_left_inj (map_nonneg _ _) (norm_nonneg _) two_ne_zero,
     Complex.sq_abs, Complex.normSq_apply, norm_sq_eq_def]
   rfl
 
@@ -400,7 +400,7 @@ instance innerProductSpace' : InnerProductSpace ℝ Vec where
   norm_sq_eq_inner v := by simp [norm_sq]
   conj_symm v₁ v₂ := by simp [Complex.conj_ofReal, mul_comm]
   add_left v₁ v₂ v₃ := by dsimp; ring
-  smul_left v₁ v₂ z := by dsimp; ring
+  smul_left v₁ v₂ z := by dsimp; simp only [zero_mul, sub_zero, add_zero, conj_trivial]; ring
 
 lemma real_inner_apply (v₁ v₂ : Vec) :
     ⟪v₁, v₂⟫_ℝ = v₁.fst * v₂.fst + v₁.snd * v₂.snd :=
@@ -694,7 +694,7 @@ lemma cdiv_eq_cdiv_iff_cdiv_eq_cdiv {v₁ v₂ v₃ v₄ : Vec} (hv₂ : v₂ 
 
 @[simp]
 lemma abs_inner (v₁ v₂ : Vec) : Complex.abs ⟪v₁, v₂⟫_ℂ = ‖v₁‖ * ‖v₂‖ := by
-  rw [← pow_left_inj (by simp) (by positivity) zero_lt_two]
+  rw [← pow_left_inj (by simp) (by positivity) two_ne_zero]
   rw [Complex.abs_apply, sq_sqrt (Complex.normSq_nonneg _)]
   dsimp [inner, det]
   rw [mul_pow, norm_sq, norm_sq]
diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean
index ee3696bb..311a19bc 100644
--- a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean
@@ -250,14 +250,12 @@ theorem CC_inx_pts_distinct {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Int
   rw [← sub_smul]
   simp
   push_neg
-  constructor
   · apply Real.sqrt_ne_zero'.mpr
     have hlt : (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2 < ω₁.radius ^ 2 := by
       apply sq_lt_sq.mpr
       rw [abs_of_pos ω₁.rad_pos]
       exact radical_axis_dist_lt_radius h
     linarith
-  exact Complex.I_ne_zero
 
 theorem CC_inx_pts_lieson_circles {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Intersect ω₂) : ((CC_Intersected_pts h).left LiesOn ω₁) ∧ ((CC_Intersected_pts h).left LiesOn ω₂) ∧ ((CC_Intersected_pts h).right LiesOn ω₁) ∧ ((CC_Intersected_pts h).right LiesOn ω₂) := by
   haveI : PtNe ω₁.center ω₂.center := ⟨ (CC_intersected_centers_distinct h) ⟩
diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean b/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean
index 149a8a4f..9ffa0d26 100644
--- a/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean
@@ -67,7 +67,28 @@ theorem neg_toDir_of_parallel_and_opposite_side {A B C D : P} {h : A ≠ B} {h
   · have : C LiesOnLeft (SEG_nd A B h.symm) ∧ D LiesOnRight (SEG_nd A B h.symm) ∨ C LiesOnRight (SEG_nd A B h.symm) ∧ D LiesOnLeft (SEG_nd A B h.symm) := by
       exact side
     rcases this with lr|rl
-    · sorry
+    · unfold IsOnLeftSide at lr
+      unfold IsOnRightSide at lr
+      have w1 : wedge C A B > 0 := by sorry
+      have w2 : wedge D A B < 0 := by sorry
+      have det1 : Vec.det (VEC A C) (VEC A B) > 0 := by sorry
+      have det2 : Vec.det (VEC B D) (VEC B A) > 0 := by sorry
+      have dir : (VEC_nd A C h₁).toDir = (VEC_nd B D h₂).toDir := by exact eq
+      have dir' : (VEC_nd A C h₁).SameDir (VEC_nd B D h₂) := by
+        apply VecND.toDir_eq_toDir_iff.mp
+        exact dir
+      unfold VecND.SameDir at dir'
+      rcases dir' with ⟨x,h⟩
+      have x_pos : x > 0 := h.1
+      have : Vec.det (VEC A C) (VEC A B) = -x * Vec.det (VEC B D) (VEC B A) := by
+        calc
+          _= x * Vec.det (VEC B D) (VEC A B) := by sorry
+          _=_ := by sorry
+      have triv : x * Vec.det (VEC B D) (VEC B A) > 0 := by positivity
+      absurd det1
+      simp only [gt_iff_lt, not_lt]
+      simp only [this]
+      linarith
     · sorry
   · exact neg
 

From c865b964f78389f8dab967c7302de3d8d9cf535c Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Fri, 12 Jan 2024 21:42:38 +0800
Subject: [PATCH 3/6] fix of bugs

---
 .../Foundation/Axiom/Basic/Plane.lean         |  1 +
 .../Foundation/Axiom/Basic/Vector.lean        |  7 ------
 .../Axiom/Position/Orientation.lean           |  3 +++
 .../Foundation/Axiom/Triangle/Basic_ex.lean   | 24 ++++++++++++++++++-
 4 files changed, 27 insertions(+), 8 deletions(-)

diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean
index 4e68873f..c33ca522 100644
--- a/EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean
@@ -49,6 +49,7 @@ theorem vadd_eq_self_iff_vec_eq_zero {A : P} {v : Vec} : v +ᵥ A = A ↔ v = 0
 theorem vec_same_eq_zero (A : P) : VEC A A = 0 := by
   rw [Vec.mkPtPt, vsub_self]
 
+@[simp]
 theorem neg_vec (A B : P) : - VEC A B = VEC B A := by
   rw [Vec.mkPtPt, Vec.mkPtPt, neg_vsub_eq_vsub_rev]
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
index 46d40460..8fbb6255 100644
--- a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean
@@ -400,14 +400,7 @@ instance innerProductSpace' : InnerProductSpace ℝ Vec where
   norm_sq_eq_inner v := by simp [norm_sq]
   conj_symm v₁ v₂ := by simp [Complex.conj_ofReal, mul_comm]
   add_left v₁ v₂ v₃ := by dsimp; ring
-<<<<<<< HEAD
   smul_left v₁ v₂ z := by dsimp; simp only [zero_mul, sub_zero, add_zero, conj_trivial]; ring
-=======
-  smul_left v₁ v₂ z := by
-    dsimp
-    simp only [zero_mul, sub_zero, add_zero, conj_trivial]
-    ring
->>>>>>> upstream/master
 
 lemma real_inner_apply (v₁ v₂ : Vec) :
     ⟪v₁, v₂⟫_ℝ = v₁.fst * v₂.fst + v₁.snd * v₂.snd :=
diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean b/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean
index 2a7bfd59..ca107a0a 100644
--- a/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean
@@ -951,6 +951,9 @@ theorem not_colinear_of_IsOnOppositeSide (A B C D : P) [bnea : PtNe B A] (h : Is
 
 end relative_side
 
+scoped notation A B "LiesOnSameSide" l => IsOnSameSide A B l
+scoped notation A B "LiesOnOppositeSide" l => IsOnOppositeSide A B l
+
 /- Position of two lines; need a function to take the intersection of two lines (when they intersect). -/
 
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean
index a7a11794..3a9101e7 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean
@@ -227,7 +227,29 @@ theorem anti_cclock_of_IsOnOppositeSide (A B C D : P) [hne : PtNe B A] (h : IsOn
   rw [this] at P
   linarith
 
-
+--LiesOnLeft or LiesOnRight straight to Angle.sign hiding cclock
+
+lemma liesonleft_ne_pts {A B C : P} [hne : PtNe B A] (h : C LiesOnLeft (DLIN A B)) : (C ≠ A) ∧ (C ≠ B) := by
+  have h': C LiesOnLeft (RAY A B) := by exact h
+  have : ¬ colinear A B C := by
+    apply not_colinear_of_LiesOnLeft_or_LiesOnRight
+    simp only [h', true_or]
+  have c_ne_a : C ≠ A := (ne_of_not_colinear this).2.1.symm
+  have c_ne_b : C ≠ B := (ne_of_not_colinear this).1
+  simp only [ne_eq, c_ne_a, not_false_eq_true, c_ne_b, and_self]
+
+lemma liesonright_ne_pts {A B C : P} [hne : PtNe B A] (h : C LiesOnRight (DLIN A B)) : (C ≠ A) ∧ (C ≠ B) := by
+  have h': C LiesOnRight (RAY A B) := by exact h
+  have : ¬ colinear A B C := by
+    apply not_colinear_of_LiesOnLeft_or_LiesOnRight
+    simp only [h', or_true]
+  have c_ne_a : C ≠ A := (ne_of_not_colinear this).2.1.symm
+  have c_ne_b : C ≠ B := (ne_of_not_colinear this).1
+  simp only [ne_eq, c_ne_a, not_false_eq_true, c_ne_b, and_self]
+
+theorem liesonright_angle_isneg {A B C : P} [hne : PtNe B A] (h : C LiesOnRight (DLIN A B)) : (∠ A C B (liesonright_ne_pts h).1.symm (liesonright_ne_pts h).2.symm).IsNeg := sorry
+
+theorem liesonleft_angle_ispos {A B C : P} [hne : PtNe B A] (h : C LiesOnLeft (DLIN A B)) : (∠ A C B (liesonleft_ne_pts h).1.symm (liesonleft_ne_pts h).2.symm).IsPos := sorry
 
 end cclock_and_odist
 

From b82c9833b615011bdb754ffd14f17b5650ff97d0 Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Fri, 12 Jan 2024 22:55:46 +0800
Subject: [PATCH 4/6] finish orientation_trash

except only one sorry proved in main file
---
 .../Axiom/Position/Orientation_trash.lean     | 381 +++++++++++++++---
 1 file changed, 321 insertions(+), 60 deletions(-)

diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean b/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean
index 9ffa0d26..ee041c84 100644
--- a/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean
@@ -17,79 +17,340 @@ theorem liesonleft_iff_liesonright_reverse {A : P} {l : DirLine P} : A LiesOnLef
     simp only [this] at P
     linarith
 
---simple corollary of "not_colinear_of_LiesOnLeft_or_LiesOnRight"
-lemma liesonleft_ne_pts {A B C : P} [hne : PtNe B A] (h : C LiesOnLeft (DLIN A B)) : (C ≠ A) ∧ (C ≠ B) := by
-  have h': C LiesOnLeft (RAY A B) := by exact h
-  have : ¬ colinear A B C := by
-    apply not_colinear_of_LiesOnLeft_or_LiesOnRight
-    simp only [h', true_or]
-  have c_ne_a : C ≠ A := (ne_of_not_colinear this).2.1.symm
-  have c_ne_b : C ≠ B := (ne_of_not_colinear this).1
-  simp only [ne_eq, c_ne_a, not_false_eq_true, c_ne_b, and_self]
-
-theorem liesonleft_angle_ispos {A B C : P} [hne : PtNe B A] (h : C LiesOnLeft (DLIN A B)) : (∠ A C B (liesonleft_ne_pts h).1.symm (liesonleft_ne_pts h).2.symm).IsPos := sorry --better to be discussed after triangle
+theorem DirLine.lieson_or_liesonleft_or_liesonright (A : P) (l : DirLine P) : (A LiesOn l) ∨ (A LiesOnLeft l) ∨ (A LiesOnRight l) := by sorry
+--Guan Nailin
+lemma eq_toDir_of_parallel_and_IsOnLL {A B C D : P} [bnea : PtNe B A] [cnea : PtNe C A] [dneb : PtNe D B] (para : (SEG_nd A C) ∥ (SEG_nd B D)) (side : C LiesOnLeft (SEG_nd A B) ∧ D LiesOnLeft (SEG_nd A B)) : (SEG_nd A C).toDir = (SEG_nd B D).toDir := by
+  have Proj : (SEG_nd A C ).toProj = (SEG_nd B D ).toProj := by
+    exact para
+  have eq_or_neg : ((SEG_nd A C ).toDir = (SEG_nd B D ).toDir) ∨ ((SEG_nd A C ).toDir = -(SEG_nd B D ).toDir) := by
+    apply Dir.toProj_eq_toProj_iff.mp
+    exact Proj
+  rcases eq_or_neg with eq|neg
+  · exact eq
+  · unfold IsOnLeftSide at side
+    have ABnd : (SEG A B).length > 0 := by
+      calc
+        _=(SEG_nd A B).length := by rfl
+        _>0 := by apply EuclidGeom.length_pos
+    have c : odist C (SEG_nd A B) > 0 := side.1
+    have d : odist D (SEG_nd A B) > 0 := side.2
+    have w1 : wedge A B C > 0 := by
+      calc
+      _= (SEG A B).length * odist' C (RAY A B) := by exact wedge_eq_length_mul_odist' A B C
+        _= (SEG A B).length * odist C (SEG_nd A B) := by rfl
+        _>0 := by positivity
+    have w2 : wedge A B D > 0 := by
+      calc
+        _= (SEG A B).length * odist' D (RAY A B) := by exact wedge_eq_length_mul_odist' A B D
+        _= (SEG A B).length * odist D (SEG_nd A B) := by rfl
+        _>0 := by positivity
+    have det1 : Vec.det (VEC A B) (VEC A C) > 0 := by
+      exact w1
+    have det2 : Vec.det (VEC B A) (VEC B D) < 0 := by
+      calc
+        _= wedge B A D := by rfl
+        _= -wedge A B D := by exact wedge213 A B D
+        _<0 := by
+          simp only [Left.neg_neg_iff]
+          exact w2
+    have dir : (VEC_nd A C ).toDir = (VEC_nd D B).toDir := by
+      have : (SEG_nd A C).toDir = (SEG_nd D B).toDir := by
+        simp only [neg]
+        symm
+        calc
+          _=(SEG_nd B D).reverse.toDir := by congr
+          _=_ := by exact EuclidGeom.SegND.toDir_of_rev_eq_neg_toDir
+      exact this
+    have dir' : (VEC_nd A C ).SameDir (VEC_nd D B ) := by
+      apply VecND.toDir_eq_toDir_iff.mp
+      exact dir
+    unfold VecND.SameDir at dir'
+    rcases dir' with ⟨x,h⟩
+    have x_pos : x > 0 := h.1
+    have h : Vec.det (VEC A B) (VEC A C) = x * Vec.det (VEC B A) (VEC B D) := by
+      calc
+        _= Vec.det (VEC A B) (x • (VEC D B)) := by
+          congr
+          exact h.2
+        _= x * Vec.det (VEC A B) (VEC D B) := by
+          simp only [LinearMap.map_smul]
+          rfl
+        _= x * Vec.det (VEC A B) (-(VEC B D)) := by
+          congr
+          simp
+        _= x * -Vec.det (VEC A B) (VEC B D) := by
+          have n: Vec.det (VEC A B) (-(VEC B D)) = -Vec.det (VEC A B) (VEC B D) := by
+            simp only [LinearMap.map_neg]
+          simp only [n]
+        _= x * -Vec.det (-(VEC B A)) (VEC B D) := by
+          congr
+          simp
+        _= x * Vec.det (VEC B A) (VEC B D) := by
+          have m: Vec.det (-(VEC B A)) (VEC B D) = -Vec.det (VEC B A) (VEC B D) := by
+            simp only [LinearMap.map_neg]
+            rfl
+          simp only [m]
+          simp only [neg_neg]
+    absurd det1
+    simp only [gt_iff_lt, not_lt]
+    simp only [h]
+    have : x * (-Vec.det (VEC B A) (VEC B D)) > 0 := by
+      have : -Vec.det (VEC B A) (VEC B D) > 0 := by
+        linarith
+      positivity
+    linarith
 
-lemma liesonright_ne_pts {A B C : P} [hne : PtNe B A] (h : C LiesOnRight (DLIN A B)) : (C ≠ A) ∧ (C ≠ B) := by
-  have h': C LiesOnRight (RAY A B) := by exact h
-  have : ¬ colinear A B C := by
-    apply not_colinear_of_LiesOnLeft_or_LiesOnRight
-    simp only [h', or_true]
-  have c_ne_a : C ≠ A := (ne_of_not_colinear this).2.1.symm
-  have c_ne_b : C ≠ B := (ne_of_not_colinear this).1
-  simp only [ne_eq, c_ne_a, not_false_eq_true, c_ne_b, and_self]
+lemma eq_toDir_of_parallel_and_IsOnRR {A B C D : P} [bnea : PtNe B A] [cnea : PtNe C A] [dneb : PtNe D B] (para : (SEG_nd A C) ∥ (SEG_nd B D)) (side : C LiesOnRight (SEG_nd A B) ∧ D LiesOnRight (SEG_nd A B)) : (SEG_nd A C).toDir = (SEG_nd B D).toDir := by
+  have Proj : (SEG_nd A C ).toProj = (SEG_nd B D ).toProj := by
+    exact para
+  have eq_or_neg : ((SEG_nd A C ).toDir = (SEG_nd B D ).toDir) ∨ ((SEG_nd A C ).toDir = -(SEG_nd B D ).toDir) := by
+    apply Dir.toProj_eq_toProj_iff.mp
+    exact Proj
+  rcases eq_or_neg with eq|neg
+  · exact eq
+  · unfold IsOnRightSide at side
+    have ABnd : (SEG A B).length > 0 := by
+      calc
+        _=(SEG_nd A B).length := by rfl
+        _>0 := by apply EuclidGeom.length_pos
+    have c : odist C (SEG_nd A B) < 0 := side.1
+    have d : odist D (SEG_nd A B) < 0 := side.2
+    have w1 : wedge A B C < 0 := by
+      calc
+      _= (SEG A B).length * odist' C (RAY A B) := by exact wedge_eq_length_mul_odist' A B C
+        _= (SEG A B).length * odist C (SEG_nd A B) := by rfl
+        _= -((SEG A B).length * -odist C (SEG_nd A B)) := by simp only [Seg.length_eq_dist, mul_neg,neg_neg]
+        _<0 := by
+          have : (SEG A B).length * -odist C (SEG_nd A B) > 0 := by
+            have : -odist C (SEG_nd A B) > 0 := by linarith
+            positivity
+          linarith
+    have w2 : wedge A B D < 0 := by
+      calc
+        _= (SEG A B).length * odist' D (RAY A B) := by exact wedge_eq_length_mul_odist' A B D
+        _= (SEG A B).length * odist D (SEG_nd A B) := by rfl
+        _<0 := by
+          have : (SEG A B).length * (-odist D (SEG_nd A B)) > 0 := by
+            have : -odist D (SEG_nd A B) > 0 := by linarith
+            positivity
+          have : (SEG A B).length * odist D (SEG_nd A B) = - ((SEG A B).length * (-odist D (SEG_nd A B))) := by simp only [Seg.length_eq_dist,mul_neg, neg_neg]
+          simp only [this]
+          linarith
+    have det1 : Vec.det (VEC A B) (VEC A C) < 0 := by
+      exact w1
+    have det2 : Vec.det (VEC B A) (VEC B D) > 0 := by
+      calc
+        _= wedge B A D := by rfl
+        _= -wedge A B D := by exact wedge213 A B D
+        _>0 := by
+          simp only [gt_iff_lt, Left.neg_pos_iff]
+          exact w2
+    have dir : (VEC_nd A C ).toDir = (VEC_nd D B).toDir := by
+      have : (SEG_nd A C).toDir = (SEG_nd D B).toDir := by
+        simp only [neg]
+        symm
+        calc
+          _=(SEG_nd B D).reverse.toDir := by congr
+          _=_ := by exact EuclidGeom.SegND.toDir_of_rev_eq_neg_toDir
+      exact this
+    have dir' : (VEC_nd A C ).SameDir (VEC_nd D B ) := by
+      apply VecND.toDir_eq_toDir_iff.mp
+      exact dir
+    unfold VecND.SameDir at dir'
+    rcases dir' with ⟨x,h⟩
+    have x_pos : x > 0 := h.1
+    have h : Vec.det (VEC A B) (VEC A C) = x * Vec.det (VEC B A) (VEC B D) := by
+      calc
+        _= Vec.det (VEC A B) (x • (VEC D B)) := by
+          congr
+          exact h.2
+        _= x * Vec.det (VEC A B) (VEC D B) := by
+          simp only [LinearMap.map_smul]
+          rfl
+        _= x * Vec.det (VEC A B) (-(VEC B D)) := by
+          congr
+          simp
+        _= x * -Vec.det (VEC A B) (VEC B D) := by
+          have n: Vec.det (VEC A B) (-(VEC B D)) = -Vec.det (VEC A B) (VEC B D) := by
+            simp only [LinearMap.map_neg]
+          simp only [n]
+        _= x * -Vec.det (-(VEC B A)) (VEC B D) := by
+          congr
+          simp
+        _= x * Vec.det (VEC B A) (VEC B D) := by
+          have m: Vec.det (-(VEC B A)) (VEC B D) = -Vec.det (VEC B A) (VEC B D) := by
+            simp only [LinearMap.map_neg]
+            rfl
+          simp only [m]
+          simp only [neg_neg]
+    absurd det1
+    simp only [not_lt]
+    simp only [h]
+    have : x * (Vec.det (VEC B A)) (VEC B D) > 0 := by
+      positivity
+    linarith
 
-theorem liesonright_angle_isneg {A B C : P} [hne : PtNe B A] (h : C LiesOnRight (DLIN A B)) : (∠ A C B (liesonright_ne_pts h).1.symm (liesonright_ne_pts h).2.symm).IsNeg := sorry --better to be discussed after triangle
+theorem eq_toDir_of_parallel_and_IsOnSameSide {A B C D : P} [bnea : PtNe B A] [cnea : PtNe C A] [dneb : PtNe D B] (para : (SEG_nd A C) ∥ (SEG_nd B D)) (side : IsOnSameSide C D (SEG_nd A B)) : (SEG_nd A C).toDir = (SEG_nd B D).toDir := by
+  unfold IsOnSameSide at side
+  unfold IsOnSameSide' at side
+  have h : C LiesOnLeft (SEG_nd A B) ∧ D LiesOnLeft (SEG_nd A B) ∨ C LiesOnRight (SEG_nd A B) ∧ D LiesOnRight (SEG_nd A B) := by exact side
+  rcases h with ll|rr
+  · exact (eq_toDir_of_parallel_and_IsOnLL para ll)
+  · exact (eq_toDir_of_parallel_and_IsOnRR para rr)
 
-theorem DirLine.lieson_or_liesonleft_or_liesonright (A : P) (l : DirLine P) : (A LiesOn l) ∨ (A LiesOnLeft l) ∨ (A LiesOnRight l) := sorry --proven in main file
 
 --Guan Nailin
-theorem eq_toDir_of_parallel_and_same_side {A B C D : P} {h : A ≠ B} {h₁ : C ≠ A} {h₂ : D ≠ B} {para : (SEG_nd A C h₁) ∥ (SEG_nd B D h₂)} {side : IsOnSameSide C D (SEG_nd A B h.symm)} : (SEG_nd A C h₁).toDir = (SEG_nd B D h₂).toDir := by
-  have Proj : (SEG_nd A C h₁).toProj = (SEG_nd B D h₂).toProj := by
+lemma neg_toDir_of_parallel_and_IsOnLR {A B C D : P} [bnea : PtNe B A] [cnea : PtNe C A] [dneb : PtNe D B] (para : (SEG_nd A C) ∥ (SEG_nd B D)) (side : C LiesOnLeft (SEG_nd A B ) ∧ D LiesOnRight (SEG_nd A B)) : (SEG_nd A C).toDir = -(SEG_nd B D).toDir := by
+  have Proj : (SEG_nd A C ).toProj = (SEG_nd B D ).toProj := by
     exact para
-  have eq_or_neg : ((SEG_nd A C h₁).toDir = (SEG_nd B D h₂).toDir) ∨ ((SEG_nd A C h₁).toDir = -(SEG_nd B D h₂).toDir) := by
+  have eq_or_neg : ((SEG_nd A C ).toDir = (SEG_nd B D ).toDir) ∨ ((SEG_nd A C ).toDir = -(SEG_nd B D ).toDir) := by
     apply Dir.toProj_eq_toProj_iff.mp
     exact Proj
   rcases eq_or_neg with eq|neg
-  · exact eq
-  · have : C LiesOnLeft (SEG_nd A B h.symm) ∧ D LiesOnLeft (SEG_nd A B h.symm) ∨ C LiesOnRight (SEG_nd A B h.symm) ∧ D LiesOnRight (SEG_nd A B h.symm) := by
-      exact side
-    rcases this with ll|rr
-    · sorry
-    · sorry
---Guan Nailin
-theorem neg_toDir_of_parallel_and_opposite_side {A B C D : P} {h : A ≠ B} {h₁ : C ≠ A} {h₂ : D ≠ B} {para : (SEG_nd A C h₁) ∥ (SEG_nd B D h₂)} {side : IsOnOppositeSide C D (SEG_nd A B h.symm)} : (SEG_nd A C h₁).toDir = -(SEG_nd B D h₂).toDir := by
-  have Proj : (SEG_nd A C h₁).toProj = (SEG_nd B D h₂).toProj := by
+  · unfold IsOnLeftSide at side
+    unfold IsOnRightSide at side
+    have ABnd : (SEG A B).length > 0 := by
+      calc
+        _=(SEG_nd A B).length := by rfl
+        _>0 := by apply EuclidGeom.length_pos
+    have c : odist C (SEG_nd A B) > 0 := side.1
+    have d : odist D (SEG_nd A B) < 0 := side.2
+    have w1 : wedge A B C > 0 := by
+      calc
+      _= (SEG A B).length * odist' C (RAY A B) := by exact wedge_eq_length_mul_odist' A B C
+        _= (SEG A B).length * odist C (SEG_nd A B) := by rfl
+        _>0 := by positivity
+    have w2 : wedge A B D < 0 := by
+      calc
+        _= (SEG A B).length * odist' D (RAY A B) := by exact wedge_eq_length_mul_odist' A B D
+        _= (SEG A B).length * odist D (SEG_nd A B) := by rfl
+        _<0 := by
+          have : (SEG A B).length * (-odist D (SEG_nd A B)) > 0 := by
+            have : -odist D (SEG_nd A B) > 0 := by linarith
+            positivity
+          have : (SEG A B).length * odist D (SEG_nd A B) = - ((SEG A B).length * (-odist D (SEG_nd A B))) := by simp only [Seg.length_eq_dist,mul_neg, neg_neg]
+          simp only [this]
+          linarith
+    have det1 : Vec.det (VEC A B) (VEC A C) > 0 := by
+      exact w1
+    have det2 : Vec.det (VEC B A) (VEC B D) > 0 := by
+      calc
+        _= wedge B A D := by rfl
+        _= -wedge A B D := by exact wedge213 A B D
+        _>0 := by
+          simp only [gt_iff_lt, Left.neg_pos_iff]
+          exact w2
+    have dir : (VEC_nd A C ).toDir = (VEC_nd B D ).toDir := by exact eq
+    have dir' : (VEC_nd A C ).SameDir (VEC_nd B D ) := by
+      apply VecND.toDir_eq_toDir_iff.mp
+      exact dir
+    unfold VecND.SameDir at dir'
+    rcases dir' with ⟨x,h⟩
+    have x_pos : x > 0 := h.1
+    have h : Vec.det (VEC A B) (VEC A C) = -x * Vec.det (VEC B A) (VEC B D) := by
+      calc
+        _= Vec.det (VEC A B) (x • (VEC B D)) := by
+          congr
+          exact h.2
+        _= x * Vec.det (VEC A B) (VEC B D) := by
+          simp only [LinearMap.map_smul]
+          rfl
+        _= x * Vec.det (-(VEC B A)) (VEC B D) := by
+          congr
+          simp
+        _= x * -Vec.det (VEC B A) (VEC B D) := by
+          have m: Vec.det (-(VEC B A)) (VEC B D) = -Vec.det (VEC B A) (VEC B D) := by
+            simp only [LinearMap.map_neg]
+            rfl
+          simp only [m]
+        _=_ := by simp only [mul_neg, neg_mul]
+    absurd det1
+    simp only [gt_iff_lt, not_lt]
+    simp only [h]
+    simp only [neg_mul, Left.neg_nonpos_iff]
+    positivity
+  · exact neg
+
+lemma neg_toDir_of_parallel_and_IsOnRL {A B C D : P} [bnea : PtNe B A] [cnea : PtNe C A] [dneb : PtNe D B] (para : (SEG_nd A C) ∥ (SEG_nd B D)) (side : C LiesOnRight (SEG_nd A B ) ∧ D LiesOnLeft (SEG_nd A B)) : (SEG_nd A C).toDir = -(SEG_nd B D).toDir := by
+  have Proj : (SEG_nd A C ).toProj = (SEG_nd B D ).toProj := by
     exact para
-  have eq_or_neg : ((SEG_nd A C h₁).toDir = (SEG_nd B D h₂).toDir) ∨ ((SEG_nd A C h₁).toDir = -(SEG_nd B D h₂).toDir) := by
+  have eq_or_neg : ((SEG_nd A C ).toDir = (SEG_nd B D ).toDir) ∨ ((SEG_nd A C ).toDir = -(SEG_nd B D ).toDir) := by
     apply Dir.toProj_eq_toProj_iff.mp
     exact Proj
   rcases eq_or_neg with eq|neg
-  · have : C LiesOnLeft (SEG_nd A B h.symm) ∧ D LiesOnRight (SEG_nd A B h.symm) ∨ C LiesOnRight (SEG_nd A B h.symm) ∧ D LiesOnLeft (SEG_nd A B h.symm) := by
-      exact side
-    rcases this with lr|rl
-    · unfold IsOnLeftSide at lr
-      unfold IsOnRightSide at lr
-      have w1 : wedge C A B > 0 := by sorry
-      have w2 : wedge D A B < 0 := by sorry
-      have det1 : Vec.det (VEC A C) (VEC A B) > 0 := by sorry
-      have det2 : Vec.det (VEC B D) (VEC B A) > 0 := by sorry
-      have dir : (VEC_nd A C h₁).toDir = (VEC_nd B D h₂).toDir := by exact eq
-      have dir' : (VEC_nd A C h₁).SameDir (VEC_nd B D h₂) := by
-        apply VecND.toDir_eq_toDir_iff.mp
-        exact dir
-      unfold VecND.SameDir at dir'
-      rcases dir' with ⟨x,h⟩
-      have x_pos : x > 0 := h.1
-      have : Vec.det (VEC A C) (VEC A B) = -x * Vec.det (VEC B D) (VEC B A) := by
-        calc
-          _= x * Vec.det (VEC B D) (VEC A B) := by sorry
-          _=_ := by sorry
-      have triv : x * Vec.det (VEC B D) (VEC B A) > 0 := by positivity
-      absurd det1
-      simp only [gt_iff_lt, not_lt]
-      simp only [this]
-      linarith
-    · sorry
+  · unfold IsOnLeftSide at side
+    unfold IsOnRightSide at side
+    have ABnd : (SEG A B).length > 0 := by
+      calc
+        _=(SEG_nd A B).length := by rfl
+        _>0 := by apply EuclidGeom.length_pos
+    have c : odist C (SEG_nd A B) < 0 := side.1
+    have d : odist D (SEG_nd A B) > 0 := side.2
+    have w1 : wedge A B C < 0 := by
+      calc
+      _= (SEG A B).length * odist' C (RAY A B) := by exact wedge_eq_length_mul_odist' A B C
+        _= (SEG A B).length * odist C (SEG_nd A B) := by rfl
+        _= -((SEG A B).length * -odist C (SEG_nd A B)) := by simp only [Seg.length_eq_dist, mul_neg,neg_neg]
+        _<0 := by
+          have : (SEG A B).length * -odist C (SEG_nd A B) > 0 := by
+            have : -odist C (SEG_nd A B) > 0 := by linarith
+            positivity
+          linarith
+    have w2 : wedge A B D > 0 := by
+      calc
+        _= (SEG A B).length * odist' D (RAY A B) := by exact wedge_eq_length_mul_odist' A B D
+        _= (SEG A B).length * odist D (SEG_nd A B) := by rfl
+        _>0 := by positivity
+    have det1 : Vec.det (VEC A B) (VEC A C) < 0 := by
+      exact w1
+    have det2 : Vec.det (VEC B A) (VEC B D) < 0 := by
+      calc
+        _= wedge B A D := by rfl
+        _= -wedge A B D := by exact wedge213 A B D
+        _<0 := by
+          simp only [Left.neg_neg_iff]
+          exact w2
+    have dir : (VEC_nd A C ).toDir = (VEC_nd B D ).toDir := by exact eq
+    have dir' : (VEC_nd A C ).SameDir (VEC_nd B D ) := by
+      apply VecND.toDir_eq_toDir_iff.mp
+      exact dir
+    unfold VecND.SameDir at dir'
+    rcases dir' with ⟨x,h⟩
+    have x_pos : x > 0 := h.1
+    have h : Vec.det (VEC A B) (VEC A C) = -x * Vec.det (VEC B A) (VEC B D) := by
+      calc
+        _= Vec.det (VEC A B) (x • (VEC B D)) := by
+          congr
+          exact h.2
+        _= x * Vec.det (VEC A B) (VEC B D) := by
+          simp only [LinearMap.map_smul]
+          rfl
+        _= x * Vec.det (-(VEC B A)) (VEC B D) := by
+          congr
+          simp
+        _= x * -Vec.det (VEC B A) (VEC B D) := by
+          have m: Vec.det (-(VEC B A)) (VEC B D) = -Vec.det (VEC B A) (VEC B D) := by
+            simp only [LinearMap.map_neg]
+            rfl
+          simp only [m]
+        _=_ := by simp only [mul_neg, neg_mul]
+    absurd det1
+    simp only [gt_iff_lt, not_lt]
+    simp only [h]
+    have : -x * Vec.det (VEC B A) (VEC B D) > 0 := by
+      have : -Vec.det (VEC B A) (VEC B D) > 0 := by linarith
+      calc
+        _= x * (-Vec.det (VEC B A) (VEC B D)) := by simp
+        _>0 := by positivity
+    linarith
   · exact neg
 
+theorem neg_toDir_of_parallel_and_IsOnOppositeSide {A B C D : P} [bnea : PtNe B A] [cnea : PtNe C A] [dneb : PtNe D B] (para : (SEG_nd A C) ∥ (SEG_nd B D)) (side : IsOnOppositeSide C D (SEG_nd A B)) : (SEG_nd A C).toDir = -(SEG_nd B D).toDir := by
+  unfold IsOnOppositeSide at side
+  unfold IsOnOppositeSide' at side
+  have h : C LiesOnLeft (SEG_nd A B) ∧ D LiesOnRight (SEG_nd A B) ∨ C LiesOnRight (SEG_nd A B) ∧ D LiesOnLeft (SEG_nd A B) := by exact side
+  rcases h with lr|rl
+  · exact (neg_toDir_of_parallel_and_IsOnLR para lr)
+  · exact (neg_toDir_of_parallel_and_IsOnRL para rl)
+
 end EuclidGeom

From e5ebf88a3e1836073fa7f35228c2d705392fb69b Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Sat, 13 Jan 2024 16:07:59 +0800
Subject: [PATCH 5/6] prove pos of left and neg on right

---
 .../Axiom/Position/Orientation.lean           | 15 ++++++-
 .../Foundation/Axiom/Triangle/Basic.lean      | 41 ++++++++++++-------
 .../Foundation/Axiom/Triangle/Basic_ex.lean   | 40 ++++++++++++++++--
 3 files changed, 76 insertions(+), 20 deletions(-)

diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean b/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean
index ca107a0a..f46c78b8 100644
--- a/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean
@@ -951,8 +951,19 @@ theorem not_colinear_of_IsOnOppositeSide (A B C D : P) [bnea : PtNe B A] (h : Is
 
 end relative_side
 
-scoped notation A B "LiesOnSameSide" l => IsOnSameSide A B l
-scoped notation A B "LiesOnOppositeSide" l => IsOnOppositeSide A B l
+scoped notation A:max "and" B:max " LiesOnSameSide " C:max => IsOnSameSide A B C
+
+variable (A B : P) [EuclideanPlane P] (l : Line P)
+
+#check A and B LiesOnSameSide l
+
+scoped notation:5 A:max "and" B:max " LiesOnOppositeSide " C:max => IsOnOppositeSide A B C
+
+
+-- @[inherit_doc IsOnSameSide]
+-- scoped syntax term:max ws term:max ws " LiesOnSameSide " ws term:max : term
+
+
 
 /- Position of two lines; need a function to take the intersection of two lines (when they intersect). -/
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
index 013c8cfb..8db4a0d2 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
@@ -263,14 +263,19 @@ end Triangle
 namespace TriangleND
 
 variable (tr_nd : TriangleND P)
---`Rewrite this Part!!!!`
-theorem angle_pos_of_cclock (cclock : tr_nd.is_cclock) : tr_nd.angle₁.value.IsPos ∧ tr_nd.angle₂.value.IsPos ∧ tr_nd.angle₃.value.IsPos := by sorry
 
-theorem angle_neg_of_clock (clock : ¬ tr_nd.is_cclock) : tr_nd.angle₁.value.IsNeg ∧ tr_nd.angle₂.value.IsNeg ∧ tr_nd.angle₃.value.IsNeg  := by sorry
+theorem angle₁_pos_iff_cclock : tr_nd.is_cclock ↔ tr_nd.angle₁.value.IsPos := by sorry
 
-theorem cclock_of_pos_angle (h : tr_nd.angle₁.value.IsPos ∨ tr_nd.angle₂.value.IsPos ∨ tr_nd.angle₃.value.IsPos) : tr_nd.is_cclock := sorry
+theorem angle₂_pos_iff_cclock : tr_nd.is_cclock ↔ tr_nd.angle₂.value.IsPos := by sorry
+
+theorem angle₃_pos_iff_cclock : tr_nd.is_cclock ↔ tr_nd.angle₃.value.IsPos := by sorry
+
+theorem angle₁_neg_iff_not_cclock : ¬ tr_nd.is_cclock ↔ tr_nd.angle₁.value.IsNeg := by sorry
+
+theorem angle₂_neg_iff_not_cclock : ¬ tr_nd.is_cclock ↔ tr_nd.angle₂.value.IsNeg := by sorry
+
+theorem angle₃_neg_iff_not_cclock : ¬ tr_nd.is_cclock ↔ tr_nd.angle₃.value.IsNeg := by sorry
 
-theorem clock_of_neg_angle (h : tr_nd.angle₁.value.IsNeg ∨ tr_nd.angle₂.value.IsNeg ∨ tr_nd.angle₃.value.IsNeg) :¬ tr_nd.is_cclock := sorry
 
 theorem pos_pos_or_neg_neg_of_iff_cclock {tr_nd₁ tr_nd₂ : TriangleND P} : (tr_nd₁.is_cclock ↔ tr_nd₂.is_cclock) ↔ (tr_nd₁.angle₁.value.IsPos ∧ tr_nd₂.angle₁.value.IsPos) ∨ (tr_nd₁.angle₁.value.IsNeg ∧ tr_nd₂.angle₁.value.IsNeg) := by
   constructor
@@ -278,25 +283,31 @@ theorem pos_pos_or_neg_neg_of_iff_cclock {tr_nd₁ tr_nd₂ : TriangleND P} : (t
     by_cases h : tr_nd₁.is_cclock
     · have h0 : tr_nd₂.is_cclock := by rw [←k] ; apply h
       left
-      exact ⟨(angle_pos_of_cclock tr_nd₁ h).1, (angle_pos_of_cclock tr_nd₂ h0).1⟩
+      --exact ⟨(angle_pos_of_cclock tr_nd₁ h).1, (angle_pos_of_cclock tr_nd₂ h0).1⟩
+      sorry
     · have h0: ¬ tr_nd₂.is_cclock := by rw [←k] ; apply h
       right
-      exact ⟨(angle_neg_of_clock tr_nd₁ h).1, (angle_neg_of_clock tr_nd₂ h0).1⟩
+      --exact ⟨(angle_neg_of_clock tr_nd₁ h).1, (angle_neg_of_clock tr_nd₂ h0).1⟩
+      sorry
   intro k
   rcases k with x | y
   · have k1 : tr_nd₁.is_cclock := by
-      apply cclock_of_pos_angle tr_nd₁
-      apply Or.inl x.1
+      --apply cclock_of_pos_angle tr_nd₁
+      --apply Or.inl x.1
+      sorry
     have k2 : tr_nd₂.is_cclock := by
-      apply cclock_of_pos_angle tr_nd₂
-      apply Or.inl x.2
+      --apply cclock_of_pos_angle tr_nd₂
+      --apply Or.inl x.2
+      sorry
     simp only [k1,k2]
   · have k1 : ¬ tr_nd₁.is_cclock := by
-      apply clock_of_neg_angle tr_nd₁
-      apply Or.inl y.1
+      --apply clock_of_neg_angle tr_nd₁
+      --apply Or.inl y.1
+      sorry
     have k2 : ¬ tr_nd₂.is_cclock := by
-      apply clock_of_neg_angle tr_nd₂
-      apply Or.inl y.2
+      --apply clock_of_neg_angle tr_nd₂
+      --apply Or.inl y.2
+      sorry
     simp only [k1,k2]
 
 theorem angle_sum_eq_pi_of_cclock (cclock : tr_nd.is_cclock): tr_nd.angle₁.value + tr_nd.angle₂.value + tr_nd.angle₃.value = π := sorry
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean
index 3a9101e7..b54b5963 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean
@@ -238,6 +238,23 @@ lemma liesonleft_ne_pts {A B C : P} [hne : PtNe B A] (h : C LiesOnLeft (DLIN A B
   have c_ne_b : C ≠ B := (ne_of_not_colinear this).1
   simp only [ne_eq, c_ne_a, not_false_eq_true, c_ne_b, and_self]
 
+theorem liesonleft_angle_ispos {A B C : P} [hne : PtNe B A] (h : C LiesOnLeft (DLIN A B)) : (∠ A C B (liesonleft_ne_pts h).1.symm (liesonleft_ne_pts h).2.symm).IsPos := by
+  have h': C LiesOnLeft (RAY A B) := by exact h
+  have ABC_nd: ¬ colinear A B C := by
+    apply not_colinear_of_LiesOnLeft_or_LiesOnRight
+    simp only [h', true_or]
+  have c : (TRI_nd A B C ABC_nd).is_cclock = C LiesOnLeft (SEG_nd A B) := by
+    apply iscclock_iff_liesonleft₃
+  have h': (TRI_nd A B C ABC_nd).is_cclock := by
+    simp only [c]
+    exact h
+  have : (TRI_nd A B C ABC_nd).angle₃.value.IsPos = (TRI_nd A B C ABC_nd).is_cclock := by
+    symm
+    simp only [eq_iff_iff]
+    exact angle₃_pos_iff_cclock (TRI_nd A B C ABC_nd)
+  simp only [← this] at h'
+  exact h'
+
 lemma liesonright_ne_pts {A B C : P} [hne : PtNe B A] (h : C LiesOnRight (DLIN A B)) : (C ≠ A) ∧ (C ≠ B) := by
   have h': C LiesOnRight (RAY A B) := by exact h
   have : ¬ colinear A B C := by
@@ -247,9 +264,26 @@ lemma liesonright_ne_pts {A B C : P} [hne : PtNe B A] (h : C LiesOnRight (DLIN A
   have c_ne_b : C ≠ B := (ne_of_not_colinear this).1
   simp only [ne_eq, c_ne_a, not_false_eq_true, c_ne_b, and_self]
 
-theorem liesonright_angle_isneg {A B C : P} [hne : PtNe B A] (h : C LiesOnRight (DLIN A B)) : (∠ A C B (liesonright_ne_pts h).1.symm (liesonright_ne_pts h).2.symm).IsNeg := sorry
-
-theorem liesonleft_angle_ispos {A B C : P} [hne : PtNe B A] (h : C LiesOnLeft (DLIN A B)) : (∠ A C B (liesonleft_ne_pts h).1.symm (liesonleft_ne_pts h).2.symm).IsPos := sorry
+theorem liesonright_angle_isneg {A B C : P} [hne : PtNe B A] (h : C LiesOnRight (DLIN A B)) : (∠ A C B (liesonright_ne_pts h).1.symm (liesonright_ne_pts h).2.symm).IsNeg := by
+  have h': C LiesOnRight (RAY A B) := by exact h
+  have h'' : C LiesOnRight (SEG_nd A B) := by exact h
+  have ABC_nd: ¬ colinear A B C := by
+    apply not_colinear_of_LiesOnLeft_or_LiesOnRight
+    simp only [h', or_true]
+  have c : (TRI_nd A B C ABC_nd).is_cclock = C LiesOnLeft (SEG_nd A B) := by
+    apply iscclock_iff_liesonleft₃
+  have H: ¬ (TRI_nd A B C ABC_nd).is_cclock := by
+    simp only [c]
+    unfold IsOnLeftSide
+    unfold IsOnRightSide at h''
+    simp only [not_lt]
+    linarith
+  have : (TRI_nd A B C ABC_nd).angle₃.value.IsNeg = ¬ (TRI_nd A B C ABC_nd).is_cclock := by
+    symm
+    simp only [eq_iff_iff]
+    exact angle₃_neg_iff_not_cclock (TRI_nd A B C ABC_nd)
+  simp only [←this] at H
+  exact H
 
 end cclock_and_odist
 

From 8d1102dd15d1ac4b3f36b1c6238a05dc790c0a4b Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Sat, 13 Jan 2024 20:49:40 +0800
Subject: [PATCH 6/6] fix the silly theorem

---
 .../Foundation/Axiom/Circle/Basic.lean        |   2 +-
 .../Foundation/Axiom/Circle/CCPosition.lean   |   5 +-
 .../Axiom/Circle/IncribedAngle.lean           |   8 +-
 .../Axiom/Position/Orientation_trash.lean     |   1 +
 .../Foundation/Axiom/Triangle/Basic.lean      |  41 ++++++-
 .../Foundation/Axiom/Triangle/Congruence.lean |  68 ++++++++----
 .../Foundation/Axiom/Triangle/Similarity.lean | 101 +++++++++++++-----
 .../Axiom/Triangle/Trigonometric.lean         |   2 +-
 8 files changed, 175 insertions(+), 53 deletions(-)

diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean
index b12a4669..1fa05a2c 100644
--- a/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean
@@ -238,7 +238,7 @@ def antipode (A : P) (ω : Circle P) : P := VEC A ω.center +ᵥ ω.center
 theorem antipode_lieson_circle {A : P} {ω : Circle P} {ha : A LiesOn ω} : (antipode A ω) LiesOn ω := by
   show dist ω.center (antipode A ω) = ω.radius
   rw [NormedAddTorsor.dist_eq_norm', antipode,  vsub_vadd_eq_vsub_sub]
-  simp
+  simp only [vsub_self, zero_sub, norm_neg]
   show ‖ω.center -ᵥ A‖ = ω.radius
   rw [← NormedAddTorsor.dist_eq_norm', ha]
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean
index 5e4f8abf..5d6939ea 100644
--- a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean
@@ -260,13 +260,14 @@ theorem CC_inx_pts_distinct {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Int
       exact radical_axis_dist_lt_radius h
     linarith
 
-theorem CC_inx_pts_lieson_circles {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Intersect ω₂) : ((CC_Intersected_pts h).left LiesOn ω₁) ∧ ((CC_Intersected_pts h).left LiesOn ω₂) ∧ ((CC_Intersected_pts h).right LiesOn ω₁) ∧ ((CC_Intersected_pts h).right LiesOn ω₂) := by
+theorem CC_inx_pts_lieson_circles' {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Intersect ω₂) : ((CC_Intersected_pts h).left LiesOn ω₁) ∧ ((CC_Intersected_pts h).left LiesOn ω₂) ∧ ((CC_Intersected_pts h).right LiesOn ω₁) ∧ ((CC_Intersected_pts h).right LiesOn ω₂) := by
   haveI : PtNe ω₁.center ω₂.center := ⟨ (CC_intersected_centers_distinct h) ⟩
   have hlt : (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2 < ω₁.radius ^ 2 := by
     apply sq_lt_sq.mpr
     rw [abs_of_pos ω₁.rad_pos]
     exact radical_axis_dist_lt_radius h
-  linarith
+  --linarith
+  sorry  --fix this
 
 theorem CC_inx_pts_lieson_circles {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Intersect ω₂) : ((CC_Intersected_pts h).left LiesOn ω₁) ∧ ((CC_Intersected_pts h).left LiesOn ω₂) ∧ ((CC_Intersected_pts h).right LiesOn ω₁) ∧ ((CC_Intersected_pts h).right LiesOn ω₂) := by
   haveI : PtNe ω₁.center ω₂.center := ⟨CC_intersected_centers_distinct h⟩
diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean b/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean
index 99d5f656..74ddaf18 100644
--- a/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean
@@ -3,6 +3,8 @@ import EuclideanGeometry.Foundation.Axiom.Position.Angle_ex2
 import EuclideanGeometry.Foundation.Axiom.Position.Orientation_trash
 import EuclideanGeometry.Foundation.Axiom.Triangle.IsocelesTriangle_trash
 import EuclideanGeometry.Foundation.Axiom.Basic.Angle_trash
+import EuclideanGeometry.Foundation.Axiom.Triangle.Basic
+import EuclideanGeometry.Foundation.Axiom.Triangle.Basic_ex
 
 noncomputable section
 namespace EuclidGeom
@@ -176,11 +178,13 @@ end angle
 
 theorem inscribed_angle_is_positive {p : P} {β : Arc P} (h : p LiesInt β.complement) : (Arc.angle_mk_pt_arc p β h.2.symm).value.IsPos := by
   unfold Arc.angle_mk_pt_arc
-  apply liesonleft_angle_ispos (Arc.liesint_complementary_arc_liesonleft_dlin h)
+  apply TriangleND.liesonleft_angle_ispos
+  exact (Arc.liesint_complementary_arc_liesonleft_dlin h)
 
 theorem inscribed_angle_of_complementary_arc_is_negative {p : P} {β : Arc P} (h : p LiesInt β) : (Arc.angle_mk_pt_arc p β h.2).value.IsNeg := by
   unfold Arc.angle_mk_pt_arc
-  apply liesonright_angle_isneg (Arc.liesint_arc_liesonright_dlin h)
+  apply TriangleND.liesonright_angle_isneg
+  exact (Arc.liesint_arc_liesonright_dlin h)
 
 theorem cangle_eq_two_times_inscribed_angle {p : P} {β : Arc P} (h₁ : p LiesOn β.circle) (h₂ : Arc.Isnot_arc_endpts p β) : β.cangle.value = 2 • (Arc.angle_mk_pt_arc p β h₂).value := by
   haveI : PtNe p β.source := ⟨h₂.1⟩
diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean b/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean
index ee041c84..3d7772ab 100644
--- a/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean
@@ -19,6 +19,7 @@ theorem liesonleft_iff_liesonright_reverse {A : P} {l : DirLine P} : A LiesOnLef
 
 theorem DirLine.lieson_or_liesonleft_or_liesonright (A : P) (l : DirLine P) : (A LiesOn l) ∨ (A LiesOnLeft l) ∨ (A LiesOnRight l) := by sorry
 --Guan Nailin
+
 lemma eq_toDir_of_parallel_and_IsOnLL {A B C D : P} [bnea : PtNe B A] [cnea : PtNe C A] [dneb : PtNe D B] (para : (SEG_nd A C) ∥ (SEG_nd B D)) (side : C LiesOnLeft (SEG_nd A B) ∧ D LiesOnLeft (SEG_nd A B)) : (SEG_nd A C).toDir = (SEG_nd B D).toDir := by
   have Proj : (SEG_nd A C ).toProj = (SEG_nd B D ).toProj := by
     exact para
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
index 8db4a0d2..c3ba7beb 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
@@ -7,6 +7,7 @@ noncomputable section
 namespace EuclidGeom
 
 open Classical
+open AngValue
 
 /- Class of generalized triangles -/
 @[ext]
@@ -264,7 +265,45 @@ namespace TriangleND
 
 variable (tr_nd : TriangleND P)
 
-theorem angle₁_pos_iff_cclock : tr_nd.is_cclock ↔ tr_nd.angle₁.value.IsPos := by sorry
+theorem angle₁_pos_iff_cclock : tr_nd.is_cclock ↔ tr_nd.angle₁.value.IsPos := by
+  simp only [← eq_iff_iff]
+  have trans1 : tr_nd.is_cclock = (tr_nd.oarea > 0) := by rfl
+  simp only [trans1]
+  have trans2 : tr_nd.oarea = wedge tr_nd.point₁ tr_nd.point₂ tr_nd.point₃ /2 := by rfl
+  simp only [trans2]
+  have trans3 : wedge tr_nd.point₁ tr_nd.point₂ tr_nd.point₃ = tr_nd.edge₃.length * tr_nd.edge₂.length * sin tr_nd.angle₁.value := by
+    calc
+      _= (SEG tr_nd.point₁ tr_nd.point₂).length * (SEG tr_nd.point₁ tr_nd.point₃).length * sin (ANG tr_nd.point₂ tr_nd.point₁ tr_nd.point₃).value := by
+        exact wedge_eq_length_mul_length_mul_sin tr_nd.point₁ tr_nd.point₂ tr_nd.point₃
+      _=_ := by
+        congr 2
+        have : (SEG tr_nd.point₁ tr_nd.point₃).length = (SEG tr_nd.point₃ tr_nd.point₁).length := by exact length_of_rev_eq_length'
+        simp only [this]
+        rfl
+  simp only [trans3]
+  have pos : (tr_nd.edge₃.length * tr_nd.edge₂.length * sin tr_nd.angle₁.value / 2 > 0) = (sin tr_nd.angle₁.value > 0) := by
+    simp only [eq_iff_iff]
+    have pos3 : tr_nd.edge₃.length > 0 := by
+      calc
+        _= tr_nd.edge_nd₃.length := by rfl
+        _>0 := by apply EuclidGeom.length_pos
+    have pos2 : tr_nd.edge₂.length > 0 := by
+      calc
+        _= tr_nd.edge_nd₂.length := by rfl
+        _>0 := by apply EuclidGeom.length_pos
+    constructor
+    · intro P
+      by_contra H
+      simp only [gt_iff_lt, not_lt] at H
+      have h : -sin tr_nd.angle₁.value ≥ 0 := by linarith
+      have : tr_nd.edge₃.length * tr_nd.edge₂.length * -sin tr_nd.angle₁.value / 2 ≥ 0 :=by
+        positivity
+      linarith
+    · intro P
+      positivity
+  simp only [pos]
+  simp only [eq_iff_iff]
+  exact isPos_iff_zero_lt_sin.symm
 
 theorem angle₂_pos_iff_cclock : tr_nd.is_cclock ↔ tr_nd.angle₂.value.IsPos := by sorry
 
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean
index b5359cdd..5687ee4f 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean
@@ -351,10 +351,10 @@ instance instHasCongr : HasCongr (TriangleND P) where
   trans := IsCongr.trans
 
 theorem is_cclock_of_cclock (h : tr_nd₁.IsCongr tr_nd₂) (cc : tr_nd₁.is_cclock) : tr_nd₂.is_cclock := by
-  apply TriangleND.cclock_of_pos_angle
-  left
+  apply (angle₁_pos_iff_cclock tr_nd₂).mpr
   rw [<-h.4]
-  exact (TriangleND.angle_pos_of_cclock tr_nd₁ cc).1
+  apply (angle₁_pos_iff_cclock tr_nd₁).mp
+  exact cc
 
 theorem area (h : tr_nd₁.IsCongr tr_nd₂) : tr_nd₁.area = tr_nd₂.area := sorry
 
@@ -420,11 +420,15 @@ structure IsACongr (tr_nd₁ tr_nd₂: TriangleND P) : Prop where intro ::
 namespace IsACongr
 
 theorem not_cclock_of_cclock (h : tr_nd₁.IsACongr tr_nd₂) (cc : tr_nd₁.is_cclock) : ¬ tr_nd₂.is_cclock := by
-  apply clock_of_neg_angle
-  left
+  apply (angle₁_pos_iff_cclock tr_nd₂).not.mpr
   have : - tr_nd₁.angle₁.value = tr_nd₂.angle₁.value := by simp only [h.4, neg_neg]
   simp only [← this, AngValue.neg_isNeg_iff_isPos]
-  exact (tr_nd₁.angle_pos_of_cclock cc).1
+  have : tr_nd₁.angle₁.value.IsPos := by
+    apply (angle₁_pos_iff_cclock tr_nd₁).mp
+    exact cc
+  simp only [neg_isPos_iff_isNeg]
+  apply AngValue.not_isNeg_of_isPos
+  exact this
 
 protected theorem symm (h : tr_nd₁.IsACongr tr_nd₂) : tr_nd₂.IsACongr tr_nd₁ where
   edge₁ := h.1.symm
@@ -712,10 +716,14 @@ theorem congr_of_SAS (e₂ : tr_nd₁.edge₂.length = tr_nd₂.edge₂.length)
   have c : tr_nd₁.is_cclock ↔ tr_nd₂.is_cclock := by
     apply TriangleND.pos_pos_or_neg_neg_of_iff_cclock.mpr
     by_cases cc: tr_nd₁.is_cclock
-    . have pos : (Angle.value (angle₁ tr_nd₁)).IsPos := (tr_nd₁.angle_pos_of_cclock cc).1
+    . have pos : (Angle.value (angle₁ tr_nd₁)).IsPos := by
+        apply (angle₁_pos_iff_cclock tr_nd₁).mp
+        exact cc
       have pos' : (Angle.value (angle₁ tr_nd₂)).IsPos := by rw [<-a₁] ; exact pos
       exact .inl ⟨pos, pos'⟩
-    . have neg : (Angle.value (angle₁ tr_nd₁)).IsNeg := (tr_nd₁.angle_neg_of_clock cc).1
+    . have neg : (Angle.value (angle₁ tr_nd₁)).IsNeg := by
+        apply (angle₁_neg_iff_not_cclock tr_nd₁).mp
+        exact cc
       have neg' : (Angle.value (angle₁ tr_nd₂)).IsNeg := by rw [<-a₁] ; exact neg
       exact .inr ⟨neg, neg'⟩
   exact congr_of_SSS_of_eq_orientation cosn₁ e₂ e₃ c
@@ -730,16 +738,22 @@ theorem acongr_of_SAS (e₂ : tr_nd₁.edge₂.length = tr_nd₂.edge₂.length)
     simp only [eq_iff_iff]
     constructor
     . intro cc
-      have pos : (Angle.value (angle₁ tr_nd₁)).IsPos := (tr_nd₁.angle_pos_of_cclock cc).1
+      have pos : (Angle.value (angle₁ tr_nd₁)).IsPos := by
+        apply (angle₁_pos_iff_cclock tr_nd₁).mp
+        exact cc
       have pos' : (Angle.value (angle₁ tr_nd₂)).IsNeg := by
         rw [a₁] at pos
         exact AngValue.neg_isPos_iff_isNeg.mp pos
-      exact tr_nd₂.clock_of_neg_angle (.inl pos')
+      apply (angle₁_neg_iff_not_cclock tr_nd₂).mpr
+      exact pos'
     intro c
     have neg' : (Angle.value (angle₁ tr_nd₁)).IsPos := by
       rw [a₁]
-      exact AngValue.neg_isPos_iff_isNeg.mpr (tr_nd₂.angle_neg_of_clock c).1
-    exact tr_nd₁.cclock_of_pos_angle (.inl neg')
+      apply AngValue.neg_isPos_iff_isNeg.mpr
+      apply (angle₁_neg_iff_not_cclock tr_nd₂).mp
+      exact c
+    apply (angle₁_pos_iff_cclock tr_nd₁).mpr
+    exact neg'
   exact acongr_of_SSS_of_ne_orientation cosn₁ e₂ e₃ c
 
 /- ASA -/
@@ -748,18 +762,18 @@ theorem congr_of_ASA (a₂ : tr_nd₁.angle₂.value = tr_nd₂.angle₂.value)
     by_cases c : tr_nd₁.is_cclock
     . have a := tr_nd₁.angle_sum_eq_pi_of_cclock c
       have c₂ : tr_nd₂.is_cclock := by
-        apply TriangleND.cclock_of_pos_angle
-        right ; left
+        apply (angle₂_pos_iff_cclock tr_nd₂).mpr
         rw [<-a₂]
-        exact (tr_nd₁.angle_pos_of_cclock c).2.1
+        apply (angle₂_pos_iff_cclock tr_nd₁).mp
+        exact c
       simp only [a₂, a₃, <- tr_nd₂.angle_sum_eq_pi_of_cclock c₂, add_left_inj] at a
       exact a
     . have a := tr_nd₁.angle_sum_eq_neg_pi_of_clock c
       have c₂ : ¬  tr_nd₂.is_cclock := by
-        apply TriangleND.clock_of_neg_angle
-        right ; left
+        apply (angle₂_neg_iff_not_cclock tr_nd₂).mpr
         rw [<-a₂]
-        exact (tr_nd₁.angle_neg_of_clock c).2.1
+        apply (angle₂_neg_iff_not_cclock tr_nd₁).mp
+        exact c
       simp only [a₂, a₃, <- tr_nd₂.angle_sum_eq_neg_pi_of_clock c₂, add_left_inj] at a
       exact a
   have e₃ : tr_nd₁.edge₃.length = tr_nd₂.edge₃.length := by
@@ -786,17 +800,27 @@ theorem acongr_of_ASA (a₂ : tr_nd₁.angle₂.value = - tr_nd₂.angle₂.valu
     by_cases c : tr_nd₁.is_cclock
     . have a := tr_nd₁.angle_sum_eq_pi_of_cclock c
       have c₂ : ¬ tr_nd₂.is_cclock := by
-        have temp := (tr_nd₁.angle_pos_of_cclock c).2.1
+        have temp : tr_nd₁.angle₂.IsPos := by
+          apply (angle₂_pos_iff_cclock tr_nd₁).mp
+          exact c
         simp only [a₂, Left.neg_pos_iff] at temp
-        exact TriangleND.clock_of_neg_angle _ (.inr (.inl (AngValue.neg_isPos_iff_isNeg.mp temp)))
+        apply (angle₂_neg_iff_not_cclock tr_nd₂).mpr
+        apply AngValue.neg_isPos_iff_isNeg.mp
+        simp only [← a₂]
+        exact temp
       simp only [a₂, a₃] at a
       have b := tr_nd₂.angle_sum_eq_neg_pi_of_clock c₂
       sorry
     . have a := tr_nd₁.angle_sum_eq_neg_pi_of_clock c
       have c₂ : tr_nd₂.is_cclock := by
-        have temp := (tr_nd₁.angle_neg_of_clock c).2.1
+        have temp : tr_nd₁.angle₂.IsNeg := by
+          apply (angle₂_neg_iff_not_cclock tr_nd₁).mp
+          exact c
         simp only [a₂, Left.neg_neg_iff] at temp
-        exact TriangleND.cclock_of_pos_angle _ (.inr (.inl (AngValue.neg_isNeg_iff_isPos.mp temp)))
+        apply (angle₂_pos_iff_cclock tr_nd₂).mpr
+        apply AngValue.neg_isNeg_iff_isPos.mp
+        simp only [← a₂]
+        exact temp
       simp only [a₂, a₃] at a
       have b := tr_nd₂.angle_sum_eq_pi_of_cclock c₂
       sorry
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Similarity.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Similarity.lean
index 761e0136..0bb10a53 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Similarity.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Similarity.lean
@@ -52,8 +52,10 @@ theorem sim_iff_perm_sim : IsSim tr₁ tr₂ ↔ IsSim (perm_vertices tr₁) (pe
   ⟨fun h ↦ h.perm_sim, fun h ↦ h.perm_sim.perm_sim⟩
 
 theorem is_cclock_of_cclock (h : IsSim tr₁ tr₂) (cc : tr₁.is_cclock) : tr₂.is_cclock := by
-  refine' cclock_of_pos_angle tr₂ (.inl _)
-  simp only [<- h.1, ( TriangleND.angle_pos_of_cclock tr₁ cc).1]
+  apply (angle₁_pos_iff_cclock tr₂).mpr
+  simp only [<- h.1]
+  apply (angle₁_pos_iff_cclock tr₁).mp
+  exact cc
 
 def ratio (_h : IsSim tr₁ tr₂) : ℝ := tr₁.edge₁.length / tr₂.edge₁.length
 
@@ -123,10 +125,13 @@ instance instHasASim : HasASim ( TriangleND P) where
   symm := IsASim.symm
 
 theorem not_cclock_of_cclock (h : IsASim tr₁ tr₂) (cc : tr₁.is_cclock) : ¬ tr₂.is_cclock := by
-  have : tr₁.angle₁.value.IsPos := (angle_pos_of_cclock tr₁ cc).1
+  have : tr₁.angle₁.value.IsPos := by
+    apply (angle₁_pos_iff_cclock tr₁).mp
+    exact cc
   rw [h.1] at this
   simp only [neg_isPos_iff_isNeg] at this
-  exact clock_of_neg_angle tr₂ (.inl this)
+  apply (angle₁_neg_iff_not_cclock tr₂).mpr
+  exact this
 
 def ratio (_h : IsASim tr₁ tr₂) : ℝ := tr₁.edge₁.length / tr₂.edge₁.length
 
@@ -224,15 +229,21 @@ theorem sim_of_AA (tr₁ tr₂ : TriangleND P) (h₂ : tr₁.angle₂.value = tr
   by_cases cc : tr₁.is_cclock
   . have : tr₂.is_cclock := by
       have : tr₂.angle₂.value.IsPos := by
-        simp only [<- h₂, ( TriangleND.angle_pos_of_cclock tr₁ cc).2.1]
-      exact cclock_of_pos_angle tr₂ (.inr (.inl this))
+        simp only [<- h₂]
+        apply (angle₂_pos_iff_cclock tr₁).mp
+        exact cc
+      apply (angle₂_pos_iff_cclock tr₂).mpr
+      exact this
     have eq₂ := angle_sum_eq_pi_of_cclock tr₂ this
     simp only [<- angle_sum_eq_pi_of_cclock tr₁ cc, h₂, h₃, add_left_inj] at eq₂
     exact eq₂.symm
   . have : ¬ tr₂.is_cclock := by
       have : tr₂.angle₂.value.IsNeg := by
-        simp only [<- h₂, ( TriangleND.angle_neg_of_clock tr₁ cc).2.1]
-      exact clock_of_neg_angle tr₂ (.inr (.inl this))
+        simp only [<- h₂]
+        apply (angle₂_neg_iff_not_cclock tr₁).mp
+        exact cc
+      apply (angle₂_neg_iff_not_cclock tr₂).mpr
+      exact this
     have eq₂ := angle_sum_eq_neg_pi_of_clock tr₂ this
     simp only [<- angle_sum_eq_neg_pi_of_clock tr₁ cc, h₂, h₃, add_left_inj] at eq₂
     exact eq₂.symm
@@ -243,19 +254,25 @@ theorem asim_of_AA (tr₁ tr₂ : TriangleND P) (h₂ : tr₁.angle₂.value = -
   constructor
   by_cases cc : tr₁.is_cclock
   . have : ¬ tr₂.is_cclock := by
-      have : tr₁.angle₂.value.IsPos := (TriangleND.angle_pos_of_cclock tr₁ cc).2.1
+      have : tr₁.angle₂.value.IsPos := by
+        apply (angle₂_pos_iff_cclock tr₁).mp
+        exact cc
       rw [h₂] at this
       simp only [neg_isPos_iff_isNeg] at this
-      exact clock_of_neg_angle tr₂ (.inr (.inl this))
+      apply (angle₂_neg_iff_not_cclock tr₂).mpr
+      exact this
     have eq₂ := angle_sum_eq_neg_pi_of_clock tr₂ this
     simp only [<- angle_sum_eq_pi_of_cclock tr₁ cc, h₂, h₃, neg_add_rev, neg_neg] at eq₂
     rw [add_comm,add_right_inj,add_comm,add_right_inj] at eq₂
     exact neg_eq_iff_eq_neg.mp (id eq₂.symm)
   . have : tr₂.is_cclock := by
-      have : tr₁.angle₂.value.IsNeg := (TriangleND.angle_neg_of_clock tr₁ cc).2.1
+      have : tr₁.angle₂.value.IsNeg := by
+        apply (angle₂_neg_iff_not_cclock tr₁).mp
+        exact cc
       rw [h₂] at this
       simp only [neg_isNeg_iff_isPos] at this
-      exact cclock_of_pos_angle tr₂ (.inr (.inl this))
+      apply (angle₂_pos_iff_cclock tr₂).mpr
+      exact this
     have eq₂ := angle_sum_eq_pi_of_cclock tr₂ this
     have eq₁ := TriangleND.angle_sum_eq_neg_pi_of_clock tr₁ cc
     simp only [h₂, h₃, <- eq₂, neg_add_rev] at eq₁
@@ -325,15 +342,23 @@ theorem sim_of_SAS (tr₁ tr₂ : TriangleND P) (e : tr₁.edge₂.length / tr
       . exact e₁
       have cc_eq := cclock_of_eq_angle tr₁ tr₂ a
       by_cases cc : tr₁.is_cclock
-      . have pos₁ : tr₁.angle₃.value.IsPos := (angle_pos_of_cclock tr₁ cc).2.2
+      . have pos₁ : tr₁.angle₃.value.IsPos := by
+          apply (angle₃_pos_iff_cclock tr₁).mp
+          exact cc
         rw [cc_eq] at cc
-        have pos₂ : tr₂.angle₃.value.IsPos := (angle_pos_of_cclock tr₂ cc).2.2
+        have pos₂ : tr₂.angle₃.value.IsPos := by
+          apply (angle₃_pos_iff_cclock tr₂).mp
+          exact cc
         have npos₁ := add_pi_isNeg_iff_isPos.mpr pos₂
         rw [<-e₂] at npos₁
         exact (not_isPos_of_isNeg npos₁ pos₁).elim
-      . have neg₁ : tr₁.angle₃.value.IsNeg := (angle_neg_of_clock tr₁ cc).2.2
+      . have neg₁ : tr₁.angle₃.value.IsNeg := by
+          apply (angle₃_neg_iff_not_cclock tr₁).mp
+          exact cc
         rw [cc_eq] at cc
-        have neg₂ : tr₂.angle₃.value.IsNeg := (angle_neg_of_clock tr₂ cc).2.2
+        have neg₂ : tr₂.angle₃.value.IsNeg := by
+          apply (angle₃_neg_iff_not_cclock tr₂).mp
+          exact cc
         have nneg₁ := add_pi_isPos_iff_isNeg.mpr neg₂
         rw [<-e₂] at nneg₁
         exact (not_isNeg_of_isPos nneg₁ neg₁).elim
@@ -360,7 +385,12 @@ theorem sim_of_SAS (tr₁ tr₂ : TriangleND P) (e : tr₁.edge₂.length / tr
     rw [two_nsmul_coe_pi] at this
     have nd := not_isND_iff_two_nsmul_eq_zero.mpr this
     rw [cclock_of_eq_angle tr₁ tr₂ a] at cc
-    exact (nd (isND_iff_isPos_or_isNeg.mpr (.inl ((angle_pos_of_cclock tr₂ cc).1)))).elim
+    exfalso
+    apply nd
+    apply isND_iff_isPos_or_isNeg.mpr
+    left
+    apply (angle₁_pos_iff_cclock tr₂).mp
+    exact cc
   have eq_pi : Angle.value tr₁.angle₂ + Angle.value tr₁.angle₃ = - π - Angle.value tr₁.angle₁ := by
       rw [<-angle_sum_eq_neg_pi_of_clock tr₁ cc] ; abel
   have eq_pi' : Angle.value tr₂.angle₂ + Angle.value tr₂.angle₃ = - π - Angle.value tr₂.angle₁ := by
@@ -374,7 +404,12 @@ theorem sim_of_SAS (tr₁ tr₂ : TriangleND P) (e : tr₁.edge₂.length / tr
   rw [neg_coe_pi,two_nsmul_coe_pi] at this
   have nd := not_isND_iff_two_nsmul_eq_zero.mpr this
   rw [cclock_of_eq_angle tr₁ tr₂ a] at cc
-  exact (nd (isND_iff_isPos_or_isNeg.mpr (.inr ((angle_neg_of_clock tr₂ cc).1)))).elim
+  exfalso
+  apply nd
+  apply isND_iff_isPos_or_isNeg.mpr
+  right
+  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
   have eq : tr₁.edge₂.length * tr₂.edge₃.length = tr₁.edge₃.length * tr₂.edge₂.length := by
@@ -440,7 +475,12 @@ theorem asim_of_SAS (tr₁ tr₂ : TriangleND P) (e : tr₁.edge₂.length / tr
       rw [<-two_smul ℕ (Angle.value tr₂.angle₁),neg_eq_zero] at eq_zero
       have nd := not_isND_iff_two_nsmul_eq_zero.mpr eq_zero
       rw [clock_of_eq_neg_angle tr₁ tr₂ a] at cc
-      exact (nd (isND_iff_isPos_or_isNeg.mpr (.inr (angle_neg_of_clock tr₂ cc).1))).elim
+      exfalso
+      apply nd
+      apply isND_iff_isPos_or_isNeg.mpr
+      right
+      apply (angle₁_neg_iff_not_cclock tr₂).mp
+      exact cc
     . have eq_zero : (Angle.value tr₂.angle₂ + Angle.value tr₂.angle₃) - (Angle.value tr₁.angle₂ + Angle.value tr₁.angle₃)  = 0 := by
         rw [<-add_sub,<-sub_sub,<-neg_neg (Angle.value tr₂.angle₃ - Angle.value tr₁.angle₂),neg_sub,<-c]
         abel
@@ -459,7 +499,12 @@ theorem asim_of_SAS (tr₁ tr₂ : TriangleND P) (e : tr₁.edge₂.length / tr
       have nd := not_isND_iff_two_nsmul_eq_zero.mpr eq_zero
       rw [clock_of_eq_neg_angle tr₁ tr₂ a] at cc
       push_neg at cc
-      exact (nd (isND_iff_isPos_or_isNeg.mpr (.inl (angle_pos_of_cclock tr₂ cc).1))).elim
+      exfalso
+      apply nd
+      apply isND_iff_isPos_or_isNeg.mpr
+      left
+      apply (angle₁_pos_iff_cclock tr₂).mp
+      exact cc
   . have : tr₁.angle₃.value = - tr₂.angle₃.value := by
       have : tr₁.angle₂.value = - (tr₂.angle₂.value + tr₂.angle₃.value) - tr₁.angle₃.value := by
         rw [<-addeq] ; abel
@@ -474,18 +519,26 @@ theorem asim_of_SAS (tr₁ tr₂ : TriangleND P) (e : tr₁.edge₂.length / tr
       . exact e₁
       have cc_eq := clock_of_eq_neg_angle tr₁ tr₂ a
       by_cases cc : tr₁.is_cclock
-      . have pos₁ : tr₁.angle₃.value.IsPos := (angle_pos_of_cclock tr₁ cc).2.2
+      . have pos₁ : tr₁.angle₃.value.IsPos := by
+          apply (angle₃_pos_iff_cclock tr₁).mp
+          exact cc
         rw [cc_eq] at cc
-        have pos₂ : tr₂.angle₃.value.IsNeg := (angle_neg_of_clock tr₂ cc).2.2
+        have pos₂ : tr₂.angle₃.value.IsNeg := by
+          apply (angle₃_neg_iff_not_cclock tr₂).mp
+          exact cc
         have pos₃ : (-tr₂.angle₃.value).IsPos := by simp only [neg_isPos_iff_isNeg,
           pos₂]
         have npos₁ := add_pi_isNeg_iff_isPos.mpr pos₃
         rw [<-e₂] at npos₁
         exact ((not_isPos_of_isNeg npos₁) pos₁).elim
-      . have neg₁ : tr₁.angle₃.value.IsNeg := (angle_neg_of_clock tr₁ cc).2.2
+      . have neg₁ : tr₁.angle₃.value.IsNeg := by
+          apply (angle₃_neg_iff_not_cclock tr₁).mp
+          exact cc
         rw [cc_eq] at cc
         push_neg at cc
-        have neg₂ : tr₂.angle₃.value.IsPos := (angle_pos_of_cclock tr₂ cc).2.2
+        have neg₂ : tr₂.angle₃.value.IsPos := by
+          apply (angle₃_pos_iff_cclock tr₂).mp
+          exact cc
         have neg₃ : (-tr₂.angle₃.value).IsNeg := by simp only [neg_isNeg_iff_isPos,
           neg₂]
         have nneg₁ := add_pi_isPos_iff_isNeg.mpr neg₃
diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean
index abc8c18d..b139f596 100644
--- a/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean
@@ -31,7 +31,7 @@ theorem cosine_rule (tr_nd : TriangleND P) : 2 * (tr_nd.edge₃.length * tr_nd.e
   let h₃ := @cosine_rule' _ _ A B C tr_nd.nontriv₃ tr_nd.nontriv₂.symm
   have h₄ : ‖VEC_nd A C tr_nd.nontriv₂.out.symm‖ = ‖VEC_nd C A tr_nd.nontriv₂.out‖
   · simp_rw [VecND.mkPtPt, ← neg_vec A C]
-    simp
+    simp only [ne_eq, VecND.mk_neg', VecND.norm_neg]
   have h₅ : Seg.length (SEG A C) = Seg.length (SEG C A)
   · rw [Seg.length_eq_norm_toVec, Seg.length_eq_norm_toVec]
     -- unfold Seg.length Seg.toVec