fix the silly theorem of cclock and angle pos

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

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]
 

EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean

@@ -400,10 +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
-    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
 
 lemma real_inner_apply (v₁ v₂ : Vec) :
     ⟪v₁, v₂⟫_ℝ = v₁.fst * v₂.fst + v₁.snd * v₂.snd :=

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]
 

EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean

@@ -253,12 +253,21 @@ theorem CC_inx_pts_distinct {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Int
   simp only [add_sub_add_right_eq_sub, sub_neg_eq_add, smul_eq_zero, add_self_eq_zero, mul_eq_zero,
     Complex.ofReal_eq_zero, Complex.I_ne_zero, or_false, VecND.ne_zero]
   push_neg
-  apply Real.sqrt_ne_zero'.mpr
+  · 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
+
+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⟩

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⟩

EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean

@@ -951,6 +951,20 @@ theorem not_colinear_of_IsOnOppositeSide (A B C D : P) [bnea : PtNe B A] (h : Is
 
 end relative_side
 
+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). -/