Modified some files to fit the new definition of Angle.

EuclideanGeometry/Foundation/Axiom/Basic/Angle.lean

@@ -32,6 +32,10 @@ instance : NormedAddCommGroup AngDValue :=
 instance : Inhabited AngDValue :=
   inferInstanceAs (Inhabited (AddCircle π))
 
+instance instCircularOrderedAddCommGroup : CircularOrderedAddCommGroup AngDValue :=
+  haveI hp : Fact (0 < π) := ⟨pi_pos⟩
+  QuotientAddGroup.instCircularOrderedAddCommGroup ℝ
+
 @[coe]
 def _root_.EuclidGeom.AngValue.toAngDValue : AngValue → AngDValue :=
   Quotient.map' id (by

EuclideanGeometry/Foundation/Axiom/Position/Angle.lean

@@ -8,6 +8,8 @@ import EuclideanGeometry.Foundation.Axiom.Basic.Angle
 
 noncomputable section
 
+open Classical
+
 namespace EuclidGeom
 
 /-- The angle value between two directed figures. -/
@@ -26,20 +28,22 @@ structure Angle (P : Type*) [EuclideanPlane P] where
 
 attribute [pp_dot] Angle.source Angle.dir₁ Angle.dir₂
 
+-- Do we need the angle between two lines, which is determined by a vertex and two `proj`s, and take values in `AngDValue`?
+
 variable {P : Type _} [EuclideanPlane P]
 
 namespace Angle
 
 alias mk_pt_dir_dir := Angle.mk
 
-/-- Given two rays with the same source, this function returns the angle consists of
-these two rays. -/
+/-- Given two rays with the same source, this function returns the angle consists of these two rays. -/
 def mk_two_ray_of_eq_source (r : Ray P) (r' : Ray P) (_h : r.source = r'.source) : Angle P where
   source := r.source
   dir₁ := r.toDir
   dir₂ := r'.toDir
 
-/-- Given vertex $O$ and two distinct points $A$ and $B$, this function returns the angle formed by rays $OA$ and $OB$. We use $\verb|ANG|$ to abbreviate $\verb|Angle.mk_pt_pt_pt|$. -/
+/-- Given vertex $O$ and two distinct points $A$ and $B$, this function returns the angle
+formed by rays $OA$ and $OB$. We use $\verb|ANG|$ to abbreviate $\verb|Angle.mk_pt_pt_pt|$. -/
 def mk_pt_pt_pt (A O B : P) (h₁ : A ≠ O) (h₂ : B ≠ O): Angle P where
   source := O
   dir₁ := (RAY O A h₁).toDir
@@ -99,7 +103,8 @@ end Angle
 
 theorem angle_value_eq_dir_angle (r r' : Ray P) (h : r.source = r'.source) : (Angle.mk_two_ray_of_eq_source r r' h).value = r'.toDir -ᵥ r.toDir := rfl
 
-/-- The value of $\verb|Angle.mk_pt_pt_pt| A O B$. We use `∠` to abbreviate $\verb|Angle.value_of_angle_of_three_point_nd|$.-/
+/-- The value of $\verb|Angle.mk_pt_pt_pt| A O B$. We use `∠` to abbreviate
+$\verb|Angle.value_of_angle_of_three_point_nd|$.-/
 abbrev value_of_angle_of_three_point_nd (A O B : P) (h₁ : A ≠ O) (h₂ : B ≠ O) : AngValue :=
   (Angle.mk_pt_pt_pt A O B h₁ h₂).value
 
@@ -160,40 +165,29 @@ def delabValueOfAngleOfThreePointND : Delab := do
     `(∠ $A $B $C)
   else
     `(∠ $A $B $C $h₁ $h₂)
-/-
+
 namespace Angle
 
+section carrier
+
 -- `should discuss this later, is there a better definition?` ite, dite is bitter to deal with
 /- `What does it mean to be LiesIn a angle? when the angle < 0`, for now it is defined as the smaller side. and when angle = π, it is defined as the left side -/
 
-protected def IsOn (p : P) (ang : Angle P) : Prop := by
-  by_cases h : p = ang.source
-  · exact True
-  · let ray := Ray.mk_pt_pt ang.source p h
-    let o₁ := Angle.mk ang.start_ray ray rfl
-    let o₂ := Angle.mk ray ang.end_ray (ang.3)
-    exact if ang.value.toReal ≥ 0 then (o₁.value.toReal ≥ 0 ∧ o₂.value.toReal ≥ 0) else (o₁.value.toReal ≤ 0 ∧ o₂.value.toReal ≤ 0)
-
-protected def IsInt (p : P) (ang : Angle P) : Prop := by
-  by_cases h : p = ang.source
-  · exact False
-  · let ray := Ray.mk_pt_pt ang.source p h
-    let o₁ := Angle.mk ang.start_ray ray rfl
-    let o₂ := Angle.mk ray ang.end_ray (ang.3)
-    exact if ang.value.toReal ≥ 0 then (o₁.value.toReal > 0 ∧ o₂.value.toReal > 0) else (o₁.value.toReal < 0 ∧ o₂.value.toReal < 0)
-
-protected theorem ison_of_isint {A : P} {ang : Angle P} : Angle.IsInt A ang → Angle.IsOn A ang := by
-  unfold Angle.IsOn Angle.IsInt
-  intro g
-  by_cases h : A = ang.source
-  · simp only [h, ge_iff_le, dite_true]
-  · simp only [h, ge_iff_le, dite_false]
-    simp only [h, ge_iff_le, gt_iff_lt, dite_false] at g
-    by_cases f : 0 ≤ ang.value.toReal
-    simp only [f, ite_true] at *
-    constructor <;> linarith
-    simp only [f, ite_false, not_false_eq_true] at *
-    constructor <;> linarith
+-- Do we need an abbreviation for `btw ang.dir₁ dir ang.dir₂`?
+
+protected def IsOn (p : P) (ang : Angle P) : Prop :=
+  if h : p = ang.source then True
+  else btw ang.dir₁ (RAY ang.source p h).toDir ang.dir₂
+
+protected structure IsInt (p : P) (ang : Angle P) : Prop where
+  ne_source : p ≠ ang.source
+  isInt : sbtw ang.dir₁ (RAY ang.source p ne_source).toDir ang.dir₂
+
+variable {p : P} {ang : Angle P}
+
+protected theorem ison_of_isint (h : ang.IsInt p) : ang.IsOn p := by
+  simp only [Angle.IsOn, h.1, dite_false]
+  exact btw_of_sbtw h.2
 
 protected def carrier (ang : Angle P) : Set P := { p : P | Angle.IsOn p ang}
 
@@ -209,13 +203,55 @@ instance : IntFig (Angle P) P where
   carrier := Angle.carrier
   interior_subset_carrier _ _ := Angle.ison_of_isint
 
-theorem lies_on_of_eq {p : P} {ang : Angle P} (h : p = ang.source) : p LiesOn ang := sorry
+theorem source_lies_on (ang : Angle P) : ang.source LiesOn ang := by
+  show if h : ang.1 = ang.1 then True else btw ang.dir₁ (RAY ang.1 ang.1 h).toDir ang.dir₂
+  simp only [dite_true]
+
+theorem lies_on_of_eq (h : p = ang.source) : p LiesOn ang := by
+  simp only [h, source_lies_on]
+
+theorem lies_on_iff_btw_of_ptNe [_h : PtNe p ang.source] : p LiesOn ang ↔ btw ang.dir₁ (RAY ang.source p).toDir ang.dir₂ :=
+  (dite_prop_iff_and _).trans ((and_iff_right (fun _ ↦ trivial)).trans (forall_prop_of_true _h.1))
+
+theorem lies_on_of_lies_on_ray_mk {d : Dir} (hd : btw ang.dir₁ d ang.dir₂) (h : p LiesOn Ray.mk ang.source d) : p LiesOn ang := sorry
+
+theorem lies_on_of_lies_on_ray {r : Ray P} (hs : ang.source = r.source) (hd : btw ang.dir₁ r.toDir ang.dir₂) (h : p LiesOn r) : p LiesOn ang :=
+  lies_on_of_lies_on_ray_mk hd ((congrArg (lies_on p) (congrFun (congrArg Ray.mk hs) r.toDir)).mpr h)
 
--- theorem lies_on_iff_btw_of_ptNe {p : P} {ang : Angle P} [_h : PtNe p ang.source] : p LiesOn ang ↔ btw
+theorem lies_on_iff_lies_on_ray : p LiesOn ang ↔ ∃ r : Ray P, (ang.source = r.source ∧ btw ang.dir₁ r.toDir ang.dir₂) ∧ p LiesOn r := sorry
+
+theorem lies_int_of_lies_int_ray_mk {d : Dir} (hd : btw ang.dir₁ d ang.dir₂) (h : p LiesInt Ray.mk ang.source d) : p LiesInt ang := sorry
+
+theorem lies_int_of_lies_int_ray {r : Ray P} (hs : ang.source = r.source) (hd : btw ang.dir₁ r.toDir ang.dir₂) (h : p LiesInt r) : p LiesInt ang :=
+  lies_int_of_lies_int_ray_mk hd ((congrArg (lies_int p) (congrFun (congrArg Ray.mk hs) r.toDir)).mpr h)
+
+theorem lies_int_iff_lies_int_ray : p LiesInt ang ↔ ∃ r : Ray P, (ang.source = r.source ∧ btw ang.dir₁ r.toDir ang.dir₂) ∧ p LiesInt r := sorry
+
+end carrier
+
+section change_dir
+
+variable (ang : Angle P) (d : Dir)
+
+def mk_dir₁: Angle P where
+  source := ang.source
+  dir₁ := ang.dir₁
+  dir₂ := d
+
+def mk_dir₂ : Angle P where
+  source := ang.source
+  dir₁ := d
+  dir₂ := ang.dir₂
+
+theorem value_mk_dir₁ : (mk_dir₁ ang d).value = d -ᵥ ang.dir₁ := rfl
+
+theorem value_mk_dir₂ : (mk_dir₂ ang d).value = ang.dir₂ -ᵥ d := rfl
+
+end change_dir
 
 end Angle
- -/
-theorem eq_end_ray_of_eq_value_eq_start_ray {ang₁ ang₂ : Angle P} (h : ang₁.start_ray = ang₂.start_ray) (v : ang₁.value = ang₂.value) : ang₁.end_ray = ang₂.end_ray := sorry /-by
+
+theorem end_ray_eq_of_value_eq_of_start_ray_eq {ang₁ ang₂ : Angle P} (h : ang₁.start_ray = ang₂.start_ray) (v : ang₁.value = ang₂.value) : ang₁.end_ray = ang₂.end_ray := sorry /-by
   ext : 1
   rw [← ang₁.source_eq_source, ← ang₂.source_eq_source, (congrArg (fun z => z.source)) h]
   let g := (congrArg (fun z => AngValue.toDir z)) v

EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean

@@ -4,9 +4,11 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Ray_trash
 
 namespace EuclidGeom
 
+open AngValue
+
 variable {P : Type _} [EuclideanPlane P]
 
-theorem sin_pos_iff_angle_pos (A : Angle P) : 0 < AngValue.sin A.value ↔ A.value.IsPos := sorry
+theorem Angle.sin_pos_iff_isPos (ang : Angle P) : 0 < sin ang.value ↔ ang.IsPos := isPos_iff_zero_lt_sin.symm
 
 theorem end_ray_toDir_rev_toDir_of_ang_rev_ang {ang₁ ang₂ : Angle P} (hs : ang₁.start_ray.toDir = (ang₂.start_ray).reverse.toDir) (h : ang₁.value = ang₂.value) : ang₁.end_ray.toDir = (ang₂.end_ray).reverse.toDir := sorry
 
@@ -30,30 +32,30 @@ theorem neg_dvalue_of_rev_ang {A B O: P} (h₁ : A ≠ O) (h₂ : B ≠ O) : (AN
 -- WangJingTing
 namespace Angle
 
-theorem end_ray_eq_value_vadd_start_ray (ang : Angle P) : ang.end_ray.toDir = ang.value +ᵥ ang.start_ray.toDir := sorry
+theorem end_ray_eq_value_vadd_start_ray (ang : Angle P) : ang.dir₂ = ang.value +ᵥ ang.dir₁ := sorry
 -- to replace
 /-
-theorem end_ray_eq_start_ray_mul_value {ang : Angle P} : ang.end_ray.toDir = ang.start_ray.toDir * ang.value.toDir := sorry
+theorem end_ray_eq_start_ray_mul_value {ang : Angle P} : ang.dir₂ = ang.dir₁ * ang.value.toDir := sorry
 -/
 
 theorem ang_source_eq_end_ray_source {ang : Angle P} : ang.source = ang.end_ray.source := sorry
 
 def mk_start_ray (ang : Angle P) (ray : Ray P) (h : ang.source = ray.source) : Angle P := Angle.mk_two_ray_of_eq_source ang.start_ray ray h
 
-def mk_ray_end (ang : Angle P) (ray : Ray P) (h : ang.source = ray.source) : Angle P := Angle.mk_two_ray_of_eq_source ray ang.end_ray (by rw[h.symm, ang_source_eq_end_ray_source])
+def mk_end_ray (ang : Angle P) (ray : Ray P) (h : ang.source = ray.source) : Angle P := Angle.mk_two_ray_of_eq_source ray ang.end_ray (by rw[h.symm, ang_source_eq_end_ray_source])
 
 theorem value_eq_vsub (ray₁ : Ray P) (ray₂ : Ray P) (h: ray₁.source = ray₂.source) : (Angle.mk_two_ray_of_eq_source ray₁ ray₂ h).value = ray₂.toDir -ᵥ ray₁.toDir := sorry
 
-theorem mk_strat_ray_value_eq_vsub (ang : Angle P) (ray : Ray P) (h : ang.source = ray.source) : (Angle.mk_start_ray ang ray h).value = ray.toDir -ᵥ ang.start_ray.toDir := sorry
+theorem mk_strat_ray_value_eq_vsub (ang : Angle P) (ray : Ray P) (h : ang.source = ray.source) : (Angle.mk_start_ray ang ray h).value = ray.toDir -ᵥ ang.dir₁ := sorry
 
-theorem mk_ray_end_value_eq_vsub (ang : Angle P) (ray : Ray P) (h : ang.source = ray.source) : (Angle.mk_ray_end ang ray h).value = ang.end_ray.toDir -ᵥ ray.toDir := sorry
+theorem mk_end_ray_value_eq_vsub (ang : Angle P) (ray : Ray P) (h : ang.source = ray.source) : (Angle.mk_end_ray ang ray h).value = ang.dir₂ -ᵥ ray.toDir := sorry
 -- to replace
 /-
 theorem value_eq_angdiff {ray₁ : Ray P} {ray₂ : Ray P} (h: ray₁.source = ray₂.source) : (Angle.mk_two_ray_of_eq_source ray₁ ray₂ h).value = Dir.AngDiff ray₁.toDir ray₂.toDir := sorry
 
-theorem mk_start_ray_value_eq_angdiff {ang : Angle P} {ray : Ray P} (h : ang.source = ray.source) : (Angle.mk_start_ray ang ray h).value = Dir.AngDiff ang.start_ray.toDir ray.toDir := sorry
+theorem mk_start_ray_value_eq_angdiff {ang : Angle P} {ray : Ray P} (h : ang.source = ray.source) : (Angle.mk_start_ray ang ray h).value = Dir.AngDiff ang.dir₁ ray.toDir := sorry
 
-theorem mk_ray_end_value_eq_angdiff {ang : Angle P} {ray : Ray P} (h : ang.source = ray.source) : (Angle.mk_ray_end ang ray h).value = Dir.AngDiff ray.toDir ang.end_ray.toDir := sorry
+theorem mk_end_ray_value_eq_angdiff {ang : Angle P} {ray : Ray P} (h : ang.source = ray.source) : (Angle.mk_end_ray ang ray h).value = Dir.AngDiff ray.toDir ang.dir₂ := sorry
 -/
 
 end Angle

EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean

@@ -7,7 +7,7 @@ import EuclideanGeometry.Foundation.Axiom.Position.Angle_trash
 noncomputable section
 namespace EuclidGeom
 
-open Classical AngValue
+open Classical AngValue Angle
 
 variable {P : Type*} [EuclideanPlane P]
 
@@ -80,11 +80,11 @@ theorem wedge_pos_iff_angle_pos (A B C : P) (nd : ¬colinear A B C) : (0 < wedge
     have h3 : 0 < sin (Angle.mk_pt_pt_pt B A C (ne_of_not_colinear nd).2.2 (ne_of_not_colinear nd).2.1.symm).value := by
       field_simp at h0
       exact h0
-    rw [sin_pos_iff_angle_pos] at h3
+    rw [sin_pos_iff_isPos] at h3
     exact h3
   rw [wedge_eq_length_mul_length_mul_sin (bnea := ⟨(ne_of_not_colinear nd).2.2⟩) (cnea := ⟨(ne_of_not_colinear nd).2.1.symm⟩)]
   intro h0
-  have h3 : 0 < sin ((Angle.mk_pt_pt_pt B A C (ne_of_not_colinear nd).2.2 (ne_of_not_colinear nd).2.1.symm).value) := (sin_pos_iff_angle_pos (Angle.mk_pt_pt_pt B A C (ne_of_not_colinear nd).2.2 (ne_of_not_colinear nd).2.1.symm)).mpr h0
+  have h3 : 0 < sin ((Angle.mk_pt_pt_pt B A C (ne_of_not_colinear nd).2.2 (ne_of_not_colinear nd).2.1.symm).value) := (sin_pos_iff_isPos (Angle.mk_pt_pt_pt B A C (ne_of_not_colinear nd).2.2 (ne_of_not_colinear nd).2.1.symm)).mpr h0
   field_simp
   exact h3
 

EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean

@@ -371,7 +371,7 @@ theorem congr_iff_perm_congr (tr_nd₁ tr_nd₂ : TriangleND P) : tr_nd₁ ≅ t
 
 theorem unique_of_eq_eq (h : tr_nd₁.IsCongr tr_nd₂) (p₁ : tr_nd₁.point₁ = tr_nd₂.point₁) (p₂ : tr_nd₁.point₂ = tr_nd₂.point₂) : tr_nd₁.point₃ = tr_nd₂.point₃ := by
   have ray_eq₁ : tr_nd₁.angle₁.end_ray = tr_nd₂.angle₁.end_ray := by
-    apply eq_end_ray_of_eq_value_eq_start_ray
+    apply end_ray_eq_of_value_eq_of_start_ray_eq
     unfold Angle.start_ray TriangleND.angle₁
     simp only [p₂, p₁] ; rfl
     exact h.4

EuclideanGeometry/Foundation/Construction/Triangle/AngleBisector.lean

@@ -12,7 +12,7 @@ import EuclideanGeometry.Foundation.Axiom.Basic.Angle_trash
 noncomputable section
 namespace EuclidGeom
 
-open AngValue
+open AngValue Angle
 
 variable {P : Type _} [EuclideanPlane P]
 
@@ -26,8 +26,9 @@ variable {P : Type _} [EuclideanPlane P]
 
 structure IsAngBis (ang : Angle P) (ray : Ray P) : Prop where
   eq_source : ang.source = ray.source
-  eq_value : (Angle.mk_start_ray ang ray eq_source).value = (Angle.mk_ray_end ang ray eq_source).value
-  -- `the definition of same_sgn should be rewrite, using btw`, i.e., `btw ang.dir₁ ray.toDir ang.dir₂`
+  eq_value : (mk_dir₁ ang ray.toDir).value = (mk_dir₂ ang ray.toDir).value
+  -- `the definition of same_sgn should be rewrite, using btw`.
+  -- For example, change it to `sbtw ang.dir₁ ray.toDir ang.dir₂ ∨ (ray.toDir =ang.dir₁ ∧ ray.toDir = ang.dir₂)`.
   same_sgn : ((Angle.mk_start_ray ang ray eq_source).value.IsPos ∧ ang.value.IsPos) ∨ ((Angle.mk_start_ray ang ray eq_source).value.IsNeg ∧ ang.value.IsNeg) ∨ ((Angle.mk_start_ray ang ray eq_source).value = ↑(π/2) ∧ ang.value = π ) ∨ ((Angle.mk_start_ray ang ray eq_source).value = 0 ∧ ang.value = 0)
 
 
@@ -44,13 +45,13 @@ namespace Angle
 /- when the Angle is flat, bis is on the left side-/
 def AngBis (ang : Angle P) : Ray P where
   source := ang.source
-  toDir := ang.value.half +ᵥ ang.start_ray.toDir
+  toDir := ang.value.half +ᵥ ang.dir₁
 
 def AngBisLine (ang : Angle P) : Line P := ang.AngBis.toLine
 
 def ExAngBis (ang : Angle P) : Ray P where
   source := ang.source
-  toDir := ∠[ang.value.toReal/2 + π/2] +ᵥ ang.start_ray.toDir
+  toDir := ∠[ang.value.toReal/2 + π/2] +ᵥ ang.dir₁
 
 def ExAngBisLine (ang : Angle P) : Line P := ang.ExAngBis.toLine
 
@@ -63,16 +64,13 @@ theorem eq_source {ang : Angle P} : ang.source = ang.AngBis.source := rfl
 theorem value_angBis_eq_half_value {ang : Angle P} : (Angle.mk_start_ray ang ang.AngBis rfl).value = ang.value.half := by
   simp only [mk_strat_ray_value_eq_vsub, AngBis, vadd_vsub]
 
-theorem  mk_start_ray_value_eq_half_angvalue {ang : Angle P} : (Angle.mk_start_ray ang ang.AngBis rfl).value.toReal = ang.value.toReal / 2 :=
+theorem mk_start_ray_value_eq_half_angvalue {ang : Angle P} : (Angle.mk_start_ray ang ang.AngBis rfl).value.toReal = ang.value.toReal / 2 :=
   (Eq.congr_right (ang.value.half_toReal).symm).mpr (congrArg toReal ang.value_angBis_eq_half_value)
 
 theorem angbis_is_angbis {ang : Angle P} : IsAngBis ang ang.AngBis where
   eq_source := rfl
   eq_value := by
-    rw [mk_strat_ray_value_eq_vsub]
-    rw [mk_ray_end_value_eq_vsub]
-    simp only [AngBis, vadd_vsub]
-    rw [vsub_vadd_eq_vsub_sub]
+    simp only [value_mk_dir₁, value_mk_dir₂, AngBis, vadd_vsub, vsub_vadd_eq_vsub_sub]
     exact sub_half_eq_half.symm
   same_sgn := by
     have g : (ang.value.IsPos) ∨ (ang.value.IsNeg) ∨ (ang.value = π) ∨ (ang.value = 0) := by
@@ -91,14 +89,14 @@ theorem angbis_is_angbis {ang : Angle P} : IsAngBis ang ang.AngBis where
       left
       constructor
       · apply toReal_eq_pi_div_two_iff.mp
-        simp only [ mk_start_ray_value_eq_half_angvalue, g₃, neg_lt_self_iff, toReal_pi]
+        simp only [mk_start_ray_value_eq_half_angvalue, g₃, neg_lt_self_iff, toReal_pi]
       · exact g₃
     · right
       right
       right
       constructor
       · rw [← AngValue.toReal_inj]
-        simp only [ mk_start_ray_value_eq_half_angvalue, g₄, toReal_zero, zero_div]
+        simp only [mk_start_ray_value_eq_half_angvalue, g₄, toReal_zero, zero_div]
       · exact g₄
 
 theorem angbis_iff_angbis {ang : Angle P} {r : Ray P} : IsAngBis ang r ↔ r = ang.AngBis := by
@@ -112,12 +110,12 @@ theorem ang_source_rev_eq_source_bis {ang : Angle P} {r : Ray P} (h : IsAngBis a
 theorem nonpi_bisector_eq_bisector_of_rev {ang : Angle P} {r : Ray P} (h : IsAngBis ang r) (nonpi : ang.value ≠ π ): IsAngBis ang.reverse r where
   eq_source := h.eq_source
   eq_value := by
-    unfold mk_start_ray mk_ray_end mk_two_ray_of_eq_source reverse start_ray end_ray value
+    simp only [value_mk_dir₁, value_mk_dir₂, reverse]
     rw [← neg_vsub_eq_vsub_rev ang.dir₂ r.toDir, ← neg_vsub_eq_vsub_rev r.toDir ang.dir₁]
     exact neg_inj.mpr h.eq_value.symm
   same_sgn := sorry /- by
-    have : (Angle.mk_start_ray ang.reverse r (ang_source_rev_eq_source_bis h)) = (Angle.mk_ray_end ang r h.eq_source).reverse := rfl
-    rw [this, (Angle.mk_ray_end ang r h.eq_source).rev_value_eq_neg_value]
+    have : (Angle.mk_start_ray ang.reverse r (ang_source_rev_eq_source_bis h)) = (Angle.mk_end_ray ang r h.eq_source).reverse := rfl
+    rw [this, (Angle.mk_end_ray ang r h.eq_source).rev_value_eq_neg_value]
     rw [ang.rev_value_eq_neg_value]
     simp
     rw [h.eq_value.symm]
@@ -170,7 +168,7 @@ namespace TriangleND
 theorem angbisline_of_angle₁_angle₂_not_parallel {tri_nd : TriangleND P} : ¬ tri_nd.angle₁.AngBis.toLine ∥ tri_nd.angle₂.AngBis.toLine := by
   by_contra g
   let A₁ := (Angle.mk_start_ray tri_nd.angle₁ tri_nd.angle₁.AngBis tri_nd.angle₁.eq_source).reverse
-  let A₂ := Angle.mk_ray_end tri_nd.angle₂ tri_nd.angle₂.AngBis tri_nd.angle₂.eq_source
+  let A₂ := Angle.mk_end_ray tri_nd.angle₂ tri_nd.angle₂.AngBis tri_nd.angle₂.eq_source
   have sr : A₁.start_ray.toDir = A₂.start_ray.toDir := by
     have h₁ : A₁.start_ray = tri_nd.angle₁.AngBis := rfl
     have h₂ : A₂.start_ray = tri_nd.angle₂.AngBis := rfl