Complete the part of Position/Angle and problem 2 of IMO in 2007 (#301)

* Clean all the trash of Position/Angle

* Changed the definitions of `ProjFig` and `DirFig`.
Now, `ProjFig` and `DirFig` extends `ProjObj` and `DirObj` respectively.

* Add the definition of sum of two angles
and the relation of `inner` and `IsAcu`, `IsRight` and `IsObt`

* Rename some theorems I have written before

* Finish statements in Position/Angle

* Fix conflicts with Linear/Order.lean

* Update Position/Angle

* Complete the part of Position/Angle

* Changed the name of right angle from `IsRight` to `IsRt`
And add definitions and basic properties of right triangles and obtuse triangles

* Add a file in order to discuss the relation between parallel and ratio

* Corrected spelling errors and added some necessary lemmas

* Add more necessary lemmas

* Finish the first draft of problem 2 of IMO in 2007

* Update problem 2 of IMO in 2007

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_3.lean

@@ -4,6 +4,8 @@ noncomputable section
 
 namespace EuclidGeom
 
+open Angle
+
 namespace Congruence_Exercise_ygr
 
 namespace Problem_3
@@ -67,21 +69,20 @@ theorem Result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : ∠
     have triv₂ : (RAY e.C e.B C_ne_B.symm) = (RAY e.C e.B C_ne_B.symm) := by rfl
     have h' : ∠ e.D e.B e.A (e.D_ne_B) (e.A_ne_B) = ∠ e.A e.C e.D (e.A_ne_C) (e.D_ne_C) := by
       calc
-        _=∠ e.D e.B e.C (e.D_ne_B) (C_ne_B) + ∠ e.C e.B e.A (C_ne_B) (e.A_ne_B)  := by
-          apply Angle.ang_eq_ang_add_ang_mod_pi_of_adj_ang (ANG  e.D e.B e.C (e.D_ne_B) (C_ne_B)) (ANG e.C e.B e.A (C_ne_B) (e.A_ne_B)) (triv₁)
-        _=-∠ e.C e.B e.D (C_ne_B) (e.D_ne_B) + ∠ e.A e.C e.B (e.A_ne_C) (C_ne_B.symm):= by
+        _= ∠ e.D e.B e.C (e.D_ne_B) (C_ne_B) + ∠ e.C e.B e.A (C_ne_B) (e.A_ne_B) := by
+          exact (value_add_eq_add_value e.B e.D e.A e.C).symm
+        _=  -∠ e.C e.B e.D (C_ne_B) (e.D_ne_B) + ∠ e.A e.C e.B (e.A_ne_C) (C_ne_B.symm) := by
           simp only [isoc_ABC_ang]
           simp only [neg_value_of_rev_ang (e.D_ne_B) (C_ne_B)]
-        _=-∠ e.D e.C e.B (e.D_ne_C) (C_ne_B.symm) + ∠ e.A e.C e.B (e.A_ne_C) (C_ne_B.symm):= by
+        _= - ∠ e.D e.C e.B (e.D_ne_C) (C_ne_B.symm) + ∠ e.A e.C e.B (e.A_ne_C) (C_ne_B.symm) := by
           simp only [isoc_DBC_ang]
-        _=∠ e.A e.C e.B (e.A_ne_C) (C_ne_B.symm) + ∠ e.B e.C e.D (C_ne_B.symm) (e.D_ne_C) := by
+        _= ∠ e.A e.C e.B (e.A_ne_C) (C_ne_B.symm) + ∠ e.B e.C e.D (C_ne_B.symm) (e.D_ne_C) := by
           simp only[neg_value_of_rev_ang (e.D_ne_C) (C_ne_B.symm)]
           abel
-        _=∠ e.A e.C e.D (e.A_ne_C) (e.D_ne_C) := by
-          symm
-          apply Angle.ang_eq_ang_add_ang_mod_pi_of_adj_ang (ANG  e.A e.C e.B (e.A_ne_C) (C_ne_B.symm)) (ANG e.B e.C e.D (C_ne_B.symm) (e.D_ne_C)) (triv₂)
+        _= ∠ e.A e.C e.D (e.A_ne_C) (e.D_ne_C) := by
+          exact value_add_eq_add_value e.C e.A e.D e.B
     simp only [← h']
-    simp only[neg_value_of_rev_ang (e.A_ne_B) (e.D_ne_B)]
+    simp only [neg_value_of_rev_ang (e.A_ne_B) (e.D_ne_B)]
   exact h
 end Problem_3
 end Congruence_Exercise_ygr

EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_6.lean

@@ -100,7 +100,7 @@ theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting2 Plane) : (S
       apply neg_value_of_rev_ang
     _= ↑ (π) + (∠ e.A e.E e.D) := by
       congr 1;
-      exact is_isoceles_tri_iff_ang_eq_ang_of_nd_tri (tri_nd := (TRI_nd e.A e.D e.E not_colinear_ADE)).mp isoceles_ADE
+      exact (is_isoceles_tri_iff_ang_eq_ang_of_nd_tri (TRI_nd e.A e.D e.E not_colinear_ADE)).mp isoceles_ADE
     _= (∠ e.D e.E e.C) + (∠ e.A e.E e.D) := by
       congr 1; symm; exact liesint_segnd_value_eq_pi' e.E_int_DC
     _= (∠ e.A e.E e.D) + (∠ e.D e.E e.C) := by abel