Corrected spelling errors and added some necessary lemmas

EuclideanGeometry/Foundation/Axiom/Circle/InscribedAngle.lean

@@ -145,7 +145,7 @@ theorem Circle.iangle_of_diameter_eq_mod_pi {ω : Circle P} {s : Chord P ω} {an
   · rw [← h]
   unfold dvalue
   rw [h, neg_div]
-  simp
+  simp only [coe_neg, AngDValue.coe_neg, AngDValue.neg_coe_pi_div_two]
 
 theorem Arc.iangle_invariant_mod_pi {ω : Circle P} {β : Arc P ω} {ang₁ ang₂ : Angle P} (h₁ : β.IsIangle ang₁) (h₂ : β.IsIangle ang₂) : ang₁.dvalue = ang₂.dvalue := by
   have : 2 • ang₁.value = 2 • ang₂.value := by
@@ -157,6 +157,18 @@ theorem Chord.iangle_invariant_mod_pi {ω : Circle P} {s : Chord P ω} {ang₁ a
     rw [← cangle_eq_two_times_inscribed_angle h₁, ← cangle_eq_two_times_inscribed_angle h₂]
   apply coe_eq_coe_iff_two_nsmul_eq.mpr this
 
+theorem Circle.dvalue_eq_of_lies_on {ω : Circle P} {A B C D : P} [_hca : PtNe C A] [_hda : PtNe D A] [_hcb : PtNe C B] [_hdb : PtNe D B] (ha : A LiesOn ω) (hb : B LiesOn ω) (hc : C LiesOn ω) (hd : D LiesOn ω) : ∡ A C B = ∡ A D B := by
+  by_cases h : B = A
+  · simp only [h, pt_pt_pt_dvalue_eq_zero_of_same_pt]
+  · haveI : PtNe B A := ⟨h⟩
+    haveI : PtNe (ARC ha hb).source (ANG A C B).source := _hca.symm
+    haveI : PtNe (ARC ha hb).target (ANG A C B).source := _hcb.symm
+    haveI : PtNe (ARC ha hb).source (ANG A D B).source := _hda.symm
+    haveI : PtNe (ARC ha hb).target (ANG A D B).source := _hdb.symm
+    apply (ARC ha hb).iangle_invariant_mod_pi
+    · exact ⟨hc, ⟨_hca.1, _hcb.1⟩, Ray.snd_pt_lies_on_mk_pt_pt, Ray.snd_pt_lies_on_mk_pt_pt⟩
+    · exact ⟨hd, ⟨_hda.1, _hdb.1⟩, Ray.snd_pt_lies_on_mk_pt_pt, Ray.snd_pt_lies_on_mk_pt_pt⟩
+
 end iangle
 
 

EuclideanGeometry/Foundation/Axiom/Linear/Line.lean

@@ -726,11 +726,11 @@ theorem ray_subset_line {r : Ray P} {l : Line P} (h : r.toLine = l) : r.carrier
   exact r.subset_toLine
 
 /-- Given a point $A$ lying on a nondegenerate segment $s$, the point $A$ also lies on the line associated to $s$. -/
-theorem seg_lies_on_line {s : SegND P} {A : P} (h : A LiesOn s) : A LiesOn s.toLine :=
+theorem SegND.lies_on_toLine {s : SegND P} {A : P} (h : A LiesOn s) : A LiesOn s.toLine :=
   Set.mem_of_subset_of_mem (ray_subset_line rfl) (SegND.lies_on_toRay_of_lies_on h)
 
 /-- The underlying set of a nondegenerate segment $s$ is a subset of the underlying set of the line associated to $s$. -/
-theorem SegND.subset_toLine {s : SegND P} : s.carrier ⊆ s.toLine.carrier := fun _ ↦ seg_lies_on_line
+theorem SegND.subset_toLine {s : SegND P} : s.carrier ⊆ s.toLine.carrier := fun _ ↦ SegND.lies_on_toLine
 
 /-- The underlying set of a nondegenerate segment is a subset of the underlying set of the line associated to the segment. -/
 theorem seg_subset_line {s : SegND P} {l : Line P} (h : s.toLine = l) : s.carrier ⊆ l.carrier := by
@@ -854,7 +854,7 @@ theorem ray_subset_dirline {r : Ray P} {l : DirLine P} (h : r.toDirLine = l) : r
 
 /-- A point $A$ lying on a nondegenerate segment $s$ also lies on the directed line associated to $s$. -/
 theorem seg_lies_on_dirline {s : SegND P} {A : P} (h : A LiesOn s.1) : A LiesOn s.toDirLine :=
-  seg_lies_on_line h
+  SegND.lies_on_toLine h
 
 /-- The underlying set of a nondegenerate segment $s$ is a subset of the underlying set of the line associated to $s$. -/
 theorem SegND.subset_toDirLine {s : SegND P} : s.carrier ⊆ s.toDirLine.carrier := s.subset_toLine
@@ -1076,6 +1076,11 @@ theorem lies_on_line_of_pt_pt_iff_collinear {A B : P} [_h : PtNe B A] (X : P) :
 theorem lies_on_iff_collinear_of_ne_lies_on_lies_on {A B : P} {l : Line P} [_h : PtNe B A] (ha : A LiesOn l) (hb : B LiesOn l) (C : P) : (C LiesOn l) ↔ Collinear A B C :=
   ⟨fun hc ↦ l.linear ha hb hc, fun c ↦ l.maximal ha hb c⟩
 
+theorem ne_pt_pt_of_not_collinear_of_lies_on {A B C : P} [_h : PtNe B A] {l : Line P} (hc : C LiesOn l) (h : ¬ Collinear A B C) : l ≠ LIN A B := by
+  contrapose! h
+  rw [h] at hc
+  exact (lies_on_line_of_pt_pt_iff_collinear C).mp hc
+
 end Line
 
 theorem exist_line_lies_on_of_collinear {A B C : P} (h : Collinear A B C) : ∃ (l : Line P), A LiesOn l ∧ B LiesOn l ∧ C LiesOn l := by

EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean

@@ -1447,6 +1447,8 @@ seg_nd.1.length + (SEG seg_nd.target A).length := by
     exact Seg.lies_on_of_lies_int h2
   rw [length_eq_length_add_length H1]
 
+theorem Seg.dist_lt_length_of_lies_int {s : Seg P} {A : P} (h : A LiesInt s) : dist s.source A < s.length := sorry
+
 end length
 
 section midpoint

EuclideanGeometry/Foundation/Axiom/Position/Angle.lean

@@ -422,9 +422,6 @@ theorem neg_value_eq_rev_ang : - ∠ A O B ha hb = ∠ B O A hb ha :=
 theorem neg_value_of_rev_ang {A O B : P} [h₁ : PtNe A O] [h₂ : PtNe B O] : ∠ A O B = -∠ B O A :=
   (neg_value_eq_rev_ang h₂.1 h₁.1).symm
 
-theorem pt_pt_pt_value_eq_zero_of_same_pt (A O : P) [PtNe A O] : ∠ A O A = 0 :=
-  vsub_self (VEC_nd O A).toDir
-
 end pt_pt_pt
 
 section mk_ray_pt
@@ -610,6 +607,10 @@ theorem angDiff_eq_zero_of_same_dir {dir₁ dir₂ : Dir} (h : dir₁ = dir₂)
 theorem same_dir_iff_value_eq_zero : ang.dir₁ = ang.dir₂ ↔ ang.value = 0 :=
   ⟨angDiff_eq_zero_of_same_dir, fun h ↦ (eq_of_vsub_eq_zero h).symm⟩
 
+@[simp]
+theorem pt_pt_pt_value_eq_zero_of_same_pt (A O : P) [PtNe A O] : ∠ A O A = 0 :=
+  vsub_self (VEC_nd O A).toDir
+
 theorem value_eq_pi_of_eq_neg_dir (h : ang.dir₁ = - ang.dir₂) : ang.value = π :=
   (eq_neg_of_vsub_eq_pi ang.dir₂ ang.dir₁).mp (by rw [h, neg_neg])
 
@@ -656,6 +657,10 @@ theorem same_proj_iff_dvalue_eq_zero : ang.proj₁ = ang.proj₂ ↔ ang.dvalue
 theorem same_proj_iff_isND : ang.proj₁ = ang.proj₂ ↔ ¬ ang.IsND :=
   same_proj_iff_dvalue_eq_zero.trans not_isND_iff_coe.symm
 
+@[simp]
+theorem pt_pt_pt_dvalue_eq_zero_of_same_pt (A O : P) [PtNe A O] : ∡ A O A = 0 :=
+  vsub_self (VEC_nd O A).toProj
+
 theorem dvalue_eq_of_dir_eq (h₁ : ang₁.dir₁ = ang₂.dir₁) (h₂ : ang₁.dir₂ = ang₂.dir₂) : ang₁.dvalue = ang₂.dvalue := by
   simp only [dvalue_eq_vsub, toProj_eq_of_eq h₁, toProj_eq_of_eq h₂]
 

EuclideanGeometry/Foundation/Index.lean

@@ -48,6 +48,7 @@ import EuclideanGeometry.Foundation.Construction.Inversion
 /- Construction.ComputationTool-/
 import EuclideanGeometry.Foundation.Construction.ComputationTool.Menelaus
 import EuclideanGeometry.Foundation.Construction.ComputationTool.Ceva
+import EuclideanGeometry.Foundation.Construction.ComputationTool.Parallel
 /- Construction.Triangle -/
 import EuclideanGeometry.Foundation.Construction.Triangle.AngleBisector
 import EuclideanGeometry.Foundation.Construction.Triangle.PerpendicularBisector