ANG

EuclideanGeometry/Check.lean

@@ -65,7 +65,7 @@ end raymk
 section anglecheck
 
 variable {P : Type _} [h : EuclideanPlane P] (O : P) (A : P) (B : P)
-#check ∠ A O B
+#check ANG A O B
 
 variable (l : GDirSeg P)
 #check l.toVec

EuclideanGeometry/Example/AOPS-Chap3.lean

@@ -43,7 +43,7 @@ let h3 := Seg.lies_int_rev_iff_lies_int.mp hx
     simp [Seg.reverse] at h3
     unfold Triangle_nd.1.edge₃
     exact (tr_nd.not_lie_on_trd_and_fst_of_int_snd h3).1
-variable (oangXBA oangYCA: OAngle P) (hoXBA : oangXBA = ∠ X B A (ne_of_not_mem_of_mem (Triangle_nd.not_lie_on_trd_and_fst_of_int_snd (eq_source_iff_lies_on_ray_lies_on_ray_rev hx).1 tr_nd.edge₃.target_lies_on) )
+variable (angXBA angYCA: Angle P) (hoXBA : angXBA = ANG X B A (ne_of_not_mem_of_mem (Triangle_nd.not_lie_on_trd_and_fst_of_int_snd (eq_source_iff_lies_on_ray_lies_on_ray_rev hx).1 tr_nd.edge₃.target_lies_on) )
 
 
 
@@ -58,10 +58,10 @@ end
 theorem notttteq : X ≠ B := by
   Triangle_nd.not_lie_on_snd_and_trd_of_int_fst
 
--- variable (oang₁ oang₂ : OAngle P) (hang1 : oang₁ = ∠ X B A)
+-- variable (ang₁ ang₂ : Angle P) (hang1 : ang₁ = ANG X B A)
 
 trind := Triangle_nd.mk (▵ A O B) hnd
-let oang₁ = ∠ 
+let ang₁ = ANG 
 end Exercise_3_4_4
 
 

EuclideanGeometry/Example/ExerciseXT8.lean

@@ -15,7 +15,7 @@ Let C be a point in the extension line of tr.point₂ tr.point₃ (i.e. tr.edge
 Let D be a point in the extension line of tr.point₁ tr.point₃ (i.e. reverse of tr.edge₂).
 Let E be a point in the extension line of tr.point₁ tr.point₂ (i.e. tr.edge₃).
 Let F be a point in the extension line of tr.point₃ tr.point₂ (i.e. reverse of tr.edge₁).
-Then ∠ tr.point₁ A B + ∠ A B tr.point₂ + ∠ tr.point₃ C D + ∠ C D tr.point₃ + ∠ tr.point₂ E F + ∠ E F tr.point₂ = 2 * π.
+Then ANG tr.point₁ A B + ANG A B tr.point₂ + ANG tr.point₃ C D + ANG C D tr.point₃ + ANG tr.point₂ E F + ANG E F tr.point₂ = 2 * π.
 -/ 
 
 example (tri : Triangle P) (nontriv : tri.is_nontriv) :
@@ -25,7 +25,7 @@ let line3 := tri.edge₁.extension_ray_of_nontriv (tri.nontriv₁ nontriv)
 let line4 := tri.edge₂.reverse.extension_ray_of_nontriv (Ne.symm (tri.nontriv₂ nontriv))
 let line5 := tri.edge₃.extension_ray_of_nontriv (tri.nontriv₃ nontriv)
 let line6 := tri.edge₁.reverse.extension_ray_of_nontriv (Ne.symm (tri.nontriv₁ nontriv))
-∀ (A B C D E F : P) [ha : A LiesInt line1] [hb : B LiesInt line2] [hc : C LiesInt line3] [hd : D LiesInt line4] [he : E LiesInt line5] [hf : F LiesInt line6], ANG tr.point₁ A B ha.2 (pts_are_distinct_of_two_rays_of_oangle )+ ANG A B tr.point₂ + ANG tr.point₃ C D + ANG C D tr.point₃ + ANG tr.point₂ E F + ANG E F tr.point₂ = 2 * π := by sorry
+∀ (A B C D E F : P) [ha : A LiesInt line1] [hb : B LiesInt line2] [hc : C LiesInt line3] [hd : D LiesInt line4] [he : E LiesInt line5] [hf : F LiesInt line6], ∠ tr.point₁ A B ha.2 (pts_are_distinct_of_two_rays_of_angle )+ ∠ A B tr.point₂ + ∠ tr.point₃ C D + ∠ C D tr.point₃ + ∠ tr.point₂ E F + ∠ E F tr.point₂ = 2 * π := by sorry
 
 end EuclidGeom
 

EuclideanGeometry/Foundation/Axiom/Position/Angle.lean

@@ -5,65 +5,63 @@ namespace EuclidGeom
 /- Define values of oriented angles, in (-π, π], modulo 2 π. -/
 /- Define oriented angles, ONLY taking in two rays starting at one point!  And define ways to construct oriented angles, by given three points on the plane, and etc.  -/
 @[ext]
-class OAngle (P : Type _) [EuclideanPlane P] where 
+class Angle (P : Type _) [EuclideanPlane P] where 
   start_ray : Ray P
   end_ray : Ray P
   source_eq_source : start_ray.source = end_ray.source
 
-namespace OAngle
+namespace Angle
 
 variable {P : Type _} [EuclideanPlane P] 
 
-def mk_pt_pt_pt (A O B : P) (h₁ : A ≠ O) (h₂ : B ≠ O): OAngle P where
+def mk_pt_pt_pt (A O B : P) (h₁ : A ≠ O) (h₂ : B ≠ O): Angle P where
   start_ray := Ray.mk_pt_pt O A h₁
   end_ray := Ray.mk_pt_pt O B h₂
   source_eq_source := rfl
 
-def mk_ray_pt (ray : Ray P) (A : P) (h : A ≠ ray.source ) : OAngle P where
+def mk_ray_pt (ray : Ray P) (A : P) (h : A ≠ ray.source ) : Angle P where
   start_ray := ray
   end_ray := Ray.mk_pt_pt ray.source A h
   source_eq_source := rfl
 
-def value (A : OAngle P): ℝ := Dir.angle (A.start_ray.toDir) (A.end_ray.toDir)
+def value (A : Angle P): ℝ := Dir.angle (A.start_ray.toDir) (A.end_ray.toDir)
 
 def angle_of_three_point_nontriv (A O B : P) (h₁ : A ≠ O) (h₂ : B ≠ O): ℝ := 
-(OAngle.mk_pt_pt_pt _ _ _ h₁ h₂).value
+(Angle.mk_pt_pt_pt _ _ _ h₁ h₂).value
 
-def angle_of_two_ray_of_eq_source (start_ray end_ray : Ray P) (h : start_ray.source = end_ray.source) : ℝ := (OAngle.mk start_ray end_ray h).value
+def angle_of_two_ray_of_eq_source (start_ray end_ray : Ray P) (h : start_ray.source = end_ray.source) : ℝ := (Angle.mk start_ray end_ray h).value
 
-def is_nd (oang : OAngle P) : Prop := oang.value ≠ 0 ∧ oang.value ≠ π 
+def is_nd (ang : Angle P) : Prop := ang.value ≠ 0 ∧ ang.value ≠ π 
 
-protected def source (oang : OAngle P) : P := oang.start_ray.source
+protected def source (ang : Angle P) : P := ang.start_ray.source
 
-end OAngle
+end Angle
 
-scoped notation "OANG" => OAngle.mk_pt_pt_pt
+scoped notation "ANG" => Angle.mk_pt_pt_pt
 
-scoped notation "ANG" => OAngle.angle_of_three_point_nontriv
+scoped notation "∠" => Angle.angle_of_three_point_nontriv
 
-scoped notation "∠" => OANG 
-
-namespace OAngle
+namespace Angle
 
 variable {P : Type _} [EuclideanPlane P] 
 
 -- `should discuss this later, is there a better definition?` ite, dite is bitter to deal with
-/- `What does it mean to be LiesIn a oangle? when the angle < 0`, for now it is defined as the smaller side. and when angle = π, it is defined as the left side -/
+/- `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 IsInt (p : P) (oang : OAngle P) : Prop := by
-  by_cases p = oang.source
+protected def IsInt (p : P) (ang : Angle P) : Prop := by
+  by_cases p = ang.source
   · exact False
-  · let ray := Ray.mk_pt_pt oang.source p h
-    let o₁ := OAngle.mk oang.start_ray ray rfl
-    let o₂ := OAngle.mk ray oang.end_ray (oang.3)
-    exact if oang.value > 0 then (o₁.value > 0 ∧ o₂.value > 0) else (o₁.value < 0 ∧ o₂.value < 0) 
+  · 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 > 0 then (o₁.value > 0 ∧ o₂.value > 0) else (o₁.value < 0 ∧ o₂.value < 0) 
 
-protected def interior (oang : OAngle P) : Set P := { p : P | OAngle.IsInt p oang }
+protected def interior (ang : Angle P) : Set P := { p : P | Angle.IsInt p ang }
 
-instance : Interior P (OAngle P) where
+instance : Interior P (Angle P) where
   interior := fun o => o.interior
 
-end OAngle
+end Angle
 
 /- theorem - π < angle.value, angle.value ≤ π,  -/
 

EuclideanGeometry/Foundation/Axiom/Position/Angle_ex.lean

@@ -6,63 +6,63 @@ noncomputable section
 
 namespace EuclidGeom
 
-namespace OAngle
+namespace Angle
 
-variable {P : Type _} [EuclideanPlane P] (oang : OAngle P)
+variable {P : Type _} [EuclideanPlane P] (ang : Angle P)
 
 /- whether an angle is acute/right/obtuse. -/
 
-def IsRightAngle {P : Type _} [EuclideanPlane P] (oang : OAngle P) : Prop := sorry
+def IsRightAngle {P : Type _} [EuclideanPlane P] (ang : Angle P) : Prop := sorry
 
 
-def IsAcuteAngle {P : Type _} [EuclideanPlane P] (oang : OAngle P) : Prop := sorry
+def IsAcuteAngle {P : Type _} [EuclideanPlane P] (ang : Angle P) : Prop := sorry
 
 
-def IsObtuseAngle {P : Type _} [EuclideanPlane P] (oang : OAngle P) : Prop := sorry
+def IsObtuseAngle {P : Type _} [EuclideanPlane P] (ang : Angle P) : Prop := sorry
 
 
 
 /- Supplementary angles -/
 
--- Define the supplementary angle to be the oangle 
+-- Define the supplementary angle to be the angle 
 
-def supplementary : (OAngle P) where
-  start_ray := oang.end_ray
-  end_ray := oang.start_ray.reverse
+def supplementary : (Angle P) where
+  start_ray := ang.end_ray
+  end_ray := ang.start_ray.reverse
   source_eq_source := sorry
 
--- If two oriented angles share a same side, then they are supplementary oriented angles if and only if the sum of two angles is π or -π   `Do I use {oang1} or (oang1)?
+-- If two oriented angles share a same side, then they are supplementary oriented angles if and only if the sum of two angles is π or -π   `Do I use {ang1} or (ang1)?
 
-theorem reverse_ray_iff_sum_of_oangle_eq_pi {oang1 : OAngle P} {oang2 : OAngle P} (h: oang1.end_ray = oang2.start_ray) : oang1.end_ray = oang2.start_ray.reverse ↔ oang1.value + oang2.value = π ∨ oang1.value + oang2.value = -π := by sorry
+theorem reverse_ray_iff_sum_of_angle_eq_pi {ang1 : Angle P} {ang2 : Angle P} (h: ang1.end_ray = ang2.start_ray) : ang1.end_ray = ang2.start_ray.reverse ↔ ang1.value + ang2.value = π ∨ ang1.value + ang2.value = -π := by sorry
 
-theorem right_of_supp_of_right (rt : IsRightAngle oang) :  IsRightAngle oang.supplementary := by sorry
+theorem right_of_supp_of_right (rt : IsRightAngle ang) :  IsRightAngle ang.supplementary := by sorry
 
-theorem acute_of_supp_of_obtuse (rt : IsObtuseAngle oang) :  IsRightAngle oang.supplementary := by sorry
+theorem acute_of_supp_of_obtuse (rt : IsObtuseAngle ang) :  IsRightAngle ang.supplementary := by sorry
 
-theorem obtuse_of_supp_of_acute (rt : IsAcuteAngle oang) :  IsRightAngle oang.supplementary := by sorry
+theorem obtuse_of_supp_of_acute (rt : IsAcuteAngle ang) :  IsRightAngle ang.supplementary := by sorry
 
-theorem is_nd_of_supp_of_is_nd (nontriv : oang.is_nd) : oang.supplementary.is_nd := by sorry
+theorem is_nd_of_supp_of_is_nd (nontriv : ang.is_nd) : ang.supplementary.is_nd := by sorry
 
-def opposite :(OAngle P) where
-  start_ray := oang.start_ray.reverse
-  end_ray := oang.end_ray.reverse
+def opposite :(Angle P) where
+  start_ray := ang.start_ray.reverse
+  end_ray := ang.end_ray.reverse
   source_eq_source := sorry
 
-theorem opposite_eq_supp_of_supp : oang.supplementary.supplementary = oang := by sorry
+theorem opposite_eq_supp_of_supp : ang.supplementary.supplementary = ang := by sorry
 
-theorem  is_nd_of_oppo_of_is_nd (nontriv : oang.is_nd) : oang.opposite.is_nd := by sorry
+theorem  is_nd_of_oppo_of_is_nd (nontriv : ang.is_nd) : ang.opposite.is_nd := by sorry
 
 
 
 
-end OAngle
+end Angle
 
-namespace OAngle
+namespace Angle
 
-variable {P : Type _} [EuclideanPlane P] (oang : OAngle P)
+variable {P : Type _} [EuclideanPlane P] (ang : Angle P)
 
 
-end OAngle
+end Angle
 
 
 end EuclidGeom

EuclideanGeometry/Foundation/Axiom/Position/Angle_ex2.lean

@@ -14,38 +14,38 @@ section AngleValue
 
 
 /- theorem - π < angle.value, angle.value ≤ π,  -/
-theorem val_gt_neg_pi (oang : OAngle P) : -π < oang.value := sorry
+theorem val_gt_neg_pi (ang : Angle P) : -π < ang.value := sorry
 
-theorem val_le_pi (oang : OAngle P) : oang.value < π := sorry
+theorem val_le_pi (ang : Angle P) : ang.value < π := sorry
 
 /- theorem when angle > 0, IsInt means lies left of start ray + right of end ray; when angle < 0, ...  -/
 
-theorem 
+theorem undefined : sorry := sorry
 
 end AngleValue
 
-section OAngleSum
+section AngleSum
 
-namespace OAngle
+namespace Angle
 
-theorem source_start_ray_eq_source_end_ray (oang : OAngle P) : oang.start_ray.source = oang.end_ray.source := sorry
+theorem source_start_ray_eq_source_end_ray (ang : Angle P) : ang.start_ray.source = ang.end_ray.source := sorry
 
 
 -- Can use congrArg @Ray.source P _) h to turn h into the sources of two terms being equal.
-theorem source_eq_source_of_adj {oang₁ oang₂: OAngle P} (h : oang₁.end_ray = oang₂.start_ray) : oang₁.start_ray.source = oang₂.end_ray.source := sorry
+theorem source_eq_source_of_adj {ang₁ ang₂: Angle P} (h : ang₁.end_ray = ang₂.start_ray) : ang₁.start_ray.source = ang₂.end_ray.source := sorry
 
 
-def sum_adj {oang₁ oang₂: OAngle P} (h :oang₁.end_ray = oang₂.start_ray) : OAngle P := OAngle.mk oang₁.start_ray oang₂.end_ray (source_eq_source_of_adj h)
+def sum_adj {ang₁ ang₂: Angle P} (h :ang₁.end_ray = ang₂.start_ray) : Angle P := Angle.mk ang₁.start_ray ang₂.end_ray (source_eq_source_of_adj h)
 
 
 
 
-theorem ang_eq_ang_add_ang_mod_pi_of_adj_oang (oang₁ oang₂ : OAngle P) (h: oang₁.end_ray = oang₂.start_ray) : (sum_adj h).value = oang₁.value + oang₂.value ∨ (sum_adj h).value = oang₁.value + oang₂.value + π ∨ (sum_adj h).value = oang₁.value + oang₂.value - π := sorry
+theorem ang_eq_ang_add_ang_mod_pi_of_adj_ang (ang₁ ang₂ : Angle P) (h: ang₁.end_ray = ang₂.start_ray) : (sum_adj h).value = ang₁.value + ang₂.value ∨ (sum_adj h).value = ang₁.value + ang₂.value + π ∨ (sum_adj h).value = ang₁.value + ang₂.value - π := sorry
 
 
 
-end OAngle 
+end Angle 
 
-end OAngleSum
+end AngleSum
 
 end EuclidGeom

EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean

@@ -15,12 +15,12 @@ section point_to_ray
 def IsOnLeftSide (A : P) (ray : Ray P) : Prop := by
   by_cases A = ray.source
   · exact False
-  · exact (0 < (OAngle.mk ray (Ray.mk_pt_pt ray.source A h ) rfl).value) ∧ ((OAngle.mk ray (Ray.mk_pt_pt ray.source A h ) rfl).value ≠ π) 
+  · exact (0 < (Angle.mk ray (Ray.mk_pt_pt ray.source A h ) rfl).value) ∧ ((Angle.mk ray (Ray.mk_pt_pt ray.source A h ) rfl).value ≠ π) 
 
 def IsOnRightSide (A : P) (ray : Ray P) : Prop := by
   by_cases A = ray.source
   · exact False
-  · exact ((OAngle.mk ray (Ray.mk_pt_pt ray.source A h ) rfl).value < 0)
+  · exact ((Angle.mk ray (Ray.mk_pt_pt ray.source A h ) rfl).value < 0)
 
 
 end point_to_ray
@@ -32,7 +32,7 @@ scoped infix : 50 "LiesOnRight" => IsOnRightSide
 section ray_to_ray
 
 /- Statement of his theorem should change, since ray₀.source ≠ ray₂.source. -/
-theorem intersect_of_ray_on_left_iff (ray₁ ray₂ : Ray P) (h : ray₂.source ≠ ray₁.source) : let ray₀ := Ray.mk_pt_pt ray₁.source ray₂.source h; (0 < OAngle.angle_of_two_ray_of_eq_source ray₀ ray₁ rfl) ∧ (OAngle.angle_of_two_ray_of_eq_source ray₀ ray₁ rfl < OAngle.angle_of_two_ray_of_eq_source ray₀ ray₂ sorry) ∧ (OAngle.angle_of_two_ray_of_eq_source ray₀ ray₂ sorry < π) ↔ (∃ A : P, (A LiesOn ray₁) ∧ (A LiesOn ray₂) ∧ (A LiesOnLeft ray₀))  := sorry
+theorem intersect_of_ray_on_left_iff (ray₁ ray₂ : Ray P) (h : ray₂.source ≠ ray₁.source) : let ray₀ := Ray.mk_pt_pt ray₁.source ray₂.source h; (0 < Angle.angle_of_two_ray_of_eq_source ray₀ ray₁ rfl) ∧ (Angle.angle_of_two_ray_of_eq_source ray₀ ray₁ rfl < Angle.angle_of_two_ray_of_eq_source ray₀ ray₂ sorry) ∧ (Angle.angle_of_two_ray_of_eq_source ray₀ ray₂ sorry < π) ↔ (∃ A : P, (A LiesOn ray₁) ∧ (A LiesOn ray₂) ∧ (A LiesOnLeft ray₀))  := sorry
 
 end ray_to_ray
 

EuclideanGeometry/Foundation/Axiom/Position/Orientation_ex.lean

@@ -8,7 +8,7 @@ namespace EuclidGeom
 
 variable {P : Type _} [EuclideanPlane P] 
 
-theorem pts_are_distinct_of_two_rays_of_oangle (oang : OAngle P) (nontriv : oang.is_nd) (A B : P) (ha : A LiesInt oang.start_ray) (hb : B LiesInt oang.end_ray) : A ≠ B := by sorry
+theorem pts_are_distinct_of_two_rays_of_angle (ang : Angle P) (nontriv : ang.is_nd) (A B : P) (ha : A LiesInt ang.start_ray) (hb : B LiesInt ang.end_ray) : A ≠ B := by sorry
 
 
 /- Position of three (distinct) points.  Giving to colinear (futher classification) -/

EuclideanGeometry/Foundation/Axiom/Position/ParallelAxiom.lean

@@ -6,10 +6,10 @@ namespace EuclidGeom
 
 variable {P : Type _} [EuclideanPlane P]
 
-theorem ang_eq_ang_of_toDir_eq_toDir {oang₁ oang₂ : OAngle P} (hs : oang₁.start_ray.toDir = oang₂.start_ray.toDir) (he : oang₁.end_ray.toDir = oang₂.end_ray.toDir) : oang₁.value = oang₂.value := sorry
+theorem ang_eq_ang_of_toDir_eq_toDir {ang₁ ang₂ : Angle P} (hs : ang₁.start_ray.toDir = ang₂.start_ray.toDir) (he : ang₁.end_ray.toDir = ang₂.end_ray.toDir) : ang₁.value = ang₂.value := sorry
 
-theorem start_ray_toDir_eq_toDir_of_ang_eq_ang {oang₁ oang₂ : OAngle P} (hs : oang₁.end_ray.toDir = oang₂.end_ray.toDir) (h : oang₁.value = oang₂.value) : oang₁.start_ray.toDir = oang₂.start_ray.toDir := sorry
+theorem start_ray_toDir_eq_toDir_of_ang_eq_ang {ang₁ ang₂ : Angle P} (hs : ang₁.end_ray.toDir = ang₂.end_ray.toDir) (h : ang₁.value = ang₂.value) : ang₁.start_ray.toDir = ang₂.start_ray.toDir := sorry
 
-theorem end_ray_toDir_eq_toDir_of_ang_eq_ang {oang₁ oang₂ : OAngle P} (hs : oang₁.start_ray.toDir = oang₂.start_ray.toDir) (h : oang₁.value = oang₂.value) : oang₁.end_ray.toDir = oang₂.end_ray.toDir := sorry
+theorem end_ray_toDir_eq_toDir_of_ang_eq_ang {ang₁ ang₂ : Angle P} (hs : ang₁.start_ray.toDir = ang₂.start_ray.toDir) (h : ang₁.value = ang₂.value) : ang₁.end_ray.toDir = ang₂.end_ray.toDir := sorry
 
 end EuclidGeom

EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean

@@ -51,17 +51,11 @@ def nontriv₃ := (ne_of_not_colinear tr_nd.2).2.2
 /- Only nondegenerate triangles can talk about orientation -/
 def is_cclock : Prop := tr_nd.1.3 LiesOnLeft (Ray.mk_pt_pt tr_nd.1.1 tr_nd.1.2 (tr_nd.nontriv₃))
 
-def oangle₁ : OAngle P := OAngle.mk_pt_pt_pt _ _ _ (tr_nd.nontriv₃) (tr_nd.nontriv₂).symm
+def angle₁ : Angle P := Angle.mk_pt_pt_pt _ _ _ (tr_nd.nontriv₃) (tr_nd.nontriv₂).symm
 
-def oangle₂ : OAngle P := OAngle.mk_pt_pt_pt _ _ _ (tr_nd.nontriv₁) (tr_nd.nontriv₃).symm
+def angle₂ : Angle P := Angle.mk_pt_pt_pt _ _ _ (tr_nd.nontriv₁) (tr_nd.nontriv₃).symm
 
-def oangle₃ : OAngle P := OAngle.mk_pt_pt_pt _ _ _ (tr_nd.nontriv₂) (tr_nd.nontriv₁).symm
-
-def angle₁ : ℝ := tr_nd.oangle₁.value
-
-def angle₂ : ℝ := tr_nd.oangle₂.value
-
-def angle₃ : ℝ := tr_nd.oangle₃.value
+def angle₃ : Angle P := Angle.mk_pt_pt_pt _ _ _ (tr_nd.nontriv₂) (tr_nd.nontriv₁).symm
 
 end Triangle_nd
 
@@ -90,17 +84,17 @@ namespace Triangle
 
 variable (tr : Triangle P) (tr_nd : Triangle_nd P)
 
-theorem angle_pos_of_cclock (cclock : tr_nd.is_cclock) : 0 < tr_nd.angle₁ ∧ 0 < tr_nd.angle₂ ∧ 0 < tr_nd.angle₃ := by sorry
+theorem angle_pos_of_cclock (cclock : tr_nd.is_cclock) : 0 < tr_nd.angle₁.value ∧ 0 < tr_nd.angle₂.value ∧ 0 < tr_nd.angle₃.value := by sorry
 
-theorem angle_neg_of_clock (clock : ¬ tr_nd.is_cclock) : tr_nd.angle₁ < 0 ∧ tr_nd.angle₂  < 0 ∧ tr_nd.angle₃ < 0  := by sorry
+theorem angle_neg_of_clock (clock : ¬ tr_nd.is_cclock) : tr_nd.angle₁.value < 0 ∧ tr_nd.angle₂.value  < 0 ∧ tr_nd.angle₃.value < 0  := by sorry
 
-theorem cclock_of_pos_angle (h : 0 < tr_nd.angle₁ ∨ 0 < tr_nd.angle₂ ∨ 0 < tr_nd.angle₃) : tr_nd.is_cclock := sorry
+theorem cclock_of_pos_angle (h : 0 < tr_nd.angle₁.value ∨ 0 < tr_nd.angle₂.value ∨ 0 < tr_nd.angle₃.value) : tr_nd.is_cclock := sorry
 
-theorem clock_of_neg_angle (h : tr_nd.angle₁ < 0 ∨ tr_nd.angle₂ < 0 ∨ tr_nd.angle₃ < 0) : tr_nd.is_cclock := sorry
+theorem clock_of_neg_angle (h : tr_nd.angle₁.value < 0 ∨ tr_nd.angle₂.value < 0 ∨ tr_nd.angle₃.value < 0) : tr_nd.is_cclock := sorry
 
-theorem angle_sum_eq_pi_of_cclock (cclock : tr_nd.is_cclock): tr_nd.angle₁ + tr_nd.angle₂ + tr_nd.angle₃ = π := sorry
+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
 
-theorem angle_sum_eq_neg_pi_of_clock (clock : ¬ tr_nd.is_cclock): tr_nd.angle₁ + tr_nd.angle₂ + tr_nd.angle₃ = - π := sorry 
+theorem angle_sum_eq_neg_pi_of_clock (clock : ¬ tr_nd.is_cclock): tr_nd.angle₁.value + tr_nd.angle₂.value + tr_nd.angle₃.value = - π := sorry 
 
 theorem triangle_ineq : tr.edge₁.length + tr.edge₂.length ≥ tr.edge₃.length := sorry