Synthetic Geometry, Euclid's Elements Book I using Avigad Axioms

In this file we prove the Pythagorean theorem (Euclid I.47) using Avigad's axioms for synthetic geometry.

theorem SyntheticEuclid4.online_of_line [I : IncidenceGeometry] (L : IncidenceGeometry.Line) : ∃ (a : IncidenceGeometry.Point), IncidenceGeometry.OnLine a L

theorem SyntheticEuclid4.online_ne_of_line [I : IncidenceGeometry] (L : IncidenceGeometry.Line) : ∃ (a : IncidenceGeometry.Point) (b : IncidenceGeometry.Point), a ≠ b ∧ IncidenceGeometry.OnLine a L ∧ IncidenceGeometry.OnLine b L

theorem SyntheticEuclid4.online_ne_of_point_line [I : IncidenceGeometry] (a : IncidenceGeometry.Point) (L : IncidenceGeometry.Line) : ∃ (b : IncidenceGeometry.Point), a ≠ b ∧ IncidenceGeometry.OnLine b L

theorem SyntheticEuclid4.len_pos_of_nq [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} (ab : a ≠ b) : 0 < IncidenceGeometry.length a b

theorem SyntheticEuclid4.ne_of_ne_len [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} (ab : a ≠ b) (ab_cd : IncidenceGeometry.length a b = IncidenceGeometry.length c d) : c ≠ d

theorem SyntheticEuclid4.ne_of_ne_len' [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} (cd : c ≠ d) (ab_cd : IncidenceGeometry.length a b = IncidenceGeometry.length c d) : a ≠ b

theorem SyntheticEuclid4.length_sum_perm_of_B [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (Babc : IncidenceGeometry.B a b c) : 0 < IncidenceGeometry.length a b ∧ 0 < IncidenceGeometry.length b c ∧ 0 < IncidenceGeometry.length a c ∧ IncidenceGeometry.length a b + IncidenceGeometry.length b c = IncidenceGeometry.length a c

theorem SyntheticEuclid4.not_online_of_line [I : IncidenceGeometry] (L : IncidenceGeometry.Line) : ∃ (a : IncidenceGeometry.Point), ¬IncidenceGeometry.OnLine a L

theorem SyntheticEuclid4.online_of_circlesinter [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {α β : IncidenceGeometry.Circle} (aα : IncidenceGeometry.CenterCircle a α) (bβ : IncidenceGeometry.CenterCircle b β) (αβ : IncidenceGeometry.CirclesInter α β) : ∃ (c : IncidenceGeometry.Point) (L : IncidenceGeometry.Line), IncidenceGeometry.OnLine a L ∧ IncidenceGeometry.OnLine b L ∧ IncidenceGeometry.OnCircle c α ∧ IncidenceGeometry.OnCircle c β ∧ ¬IncidenceGeometry.OnLine c L

theorem SyntheticEuclid4.not_sameside_symm [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (abL : ¬IncidenceGeometry.SameSide a b L) : ¬IncidenceGeometry.SameSide b a L

theorem SyntheticEuclid4.diffside_symm [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (abL : diffside a b L) : diffside b a L

theorem SyntheticEuclid4.diffside_of_sameside_diffside [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (abL : IncidenceGeometry.SameSide a b L) (acL : diffside a c L) : diffside b c L

theorem SyntheticEuclid4.sameside_of_diffside_diffside [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (abL : diffside a b L) (acL : diffside a c L) : IncidenceGeometry.SameSide b c L

theorem SyntheticEuclid4.diffside_of_circlesinter [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {α β : IncidenceGeometry.Circle} (aα : IncidenceGeometry.CenterCircle a α) (bβ : IncidenceGeometry.CenterCircle b β) (αβ : IncidenceGeometry.CirclesInter α β) : ∃ (c : IncidenceGeometry.Point) (d : IncidenceGeometry.Point) (L : IncidenceGeometry.Line), IncidenceGeometry.OnLine a L ∧ IncidenceGeometry.OnLine b L ∧ IncidenceGeometry.OnCircle c α ∧ IncidenceGeometry.OnCircle c β ∧ IncidenceGeometry.OnCircle d α ∧ IncidenceGeometry.OnCircle d β ∧ diffside c d L

theorem SyntheticEuclid4.online_of_col_online [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (ab : a ≠ b) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (col_abc : colinear a b c) : IncidenceGeometry.OnLine c L

theorem SyntheticEuclid4.triangle_of_ne_online [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (ab : a ≠ b) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (cL : ¬IncidenceGeometry.OnLine c L) : triangle a b c

theorem SyntheticEuclid4.online_3_of_triangle [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (tri_abc : triangle a b c) : ¬IncidenceGeometry.OnLine c L

theorem SyntheticEuclid4.online_1_of_triangle [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (bL : IncidenceGeometry.OnLine b L) (cL : IncidenceGeometry.OnLine c L) (tri_abc : triangle a b c) : ¬IncidenceGeometry.OnLine a L

theorem SyntheticEuclid4.online_2_of_triangle [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (aL : IncidenceGeometry.OnLine a L) (cL : IncidenceGeometry.OnLine c L) (tri_abc : triangle a b c) : ¬IncidenceGeometry.OnLine b L

theorem SyntheticEuclid4.eq_tri_of_length_online [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (ab : a ≠ b) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (cL : ¬IncidenceGeometry.OnLine c L) (ab_ac : IncidenceGeometry.length a b = IncidenceGeometry.length a c) (bc_ba : IncidenceGeometry.length b c = IncidenceGeometry.length b a) : eqTri a b c

theorem SyntheticEuclid4.B_circ_of_ne [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (ab : a ≠ b) (bc : b ≠ c) : ∃ (d : IncidenceGeometry.Point) (α : IncidenceGeometry.Circle), IncidenceGeometry.B a b d ∧ IncidenceGeometry.CenterCircle b α ∧ IncidenceGeometry.OnCircle c α ∧ IncidenceGeometry.OnCircle d α

theorem SyntheticEuclid4.online_of_eq [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (ab : a = b) (aL : IncidenceGeometry.OnLine a L) : IncidenceGeometry.OnLine b L

theorem SyntheticEuclid4.online_of_eq' [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (ab : a = b) (bL : IncidenceGeometry.OnLine b L) : IncidenceGeometry.OnLine a L

theorem SyntheticEuclid4.ne_12_of_tri [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri : triangle a b c) : a ≠ b

theorem SyntheticEuclid4.ne_21_of_tri [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri : triangle a b c) : b ≠ a

theorem SyntheticEuclid4.ne_23_of_tri [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri : triangle a b c) : b ≠ c

theorem SyntheticEuclid4.ne_32_of_tri [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri : triangle a b c) : c ≠ b

theorem SyntheticEuclid4.ne_13_of_tri [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri : triangle a b c) : a ≠ c

theorem SyntheticEuclid4.ne_31_of_tri [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri : triangle a b c) : c ≠ a

theorem SyntheticEuclid4.incirc_of_lt [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {α : IncidenceGeometry.Circle} (aα : IncidenceGeometry.CenterCircle a α) (bα : IncidenceGeometry.OnCircle b α) (ac_ab : IncidenceGeometry.length a c < IncidenceGeometry.length a b) : IncidenceGeometry.InCircle c α

theorem SyntheticEuclid4.B_circ_out_of_B [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} (ab : a ≠ b) (Bacd : IncidenceGeometry.B a c d) (ab_ac : IncidenceGeometry.length a b = IncidenceGeometry.length a c) : ∃ (e : IncidenceGeometry.Point) (α : IncidenceGeometry.Circle), IncidenceGeometry.B a b e ∧ IncidenceGeometry.CenterCircle a α ∧ IncidenceGeometry.OnCircle d α ∧ IncidenceGeometry.OnCircle e α

theorem SyntheticEuclid4.length_eq_of_oncircle [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {α : IncidenceGeometry.Circle} (aα : IncidenceGeometry.CenterCircle a α) (bα : IncidenceGeometry.OnCircle b α) (cα : IncidenceGeometry.OnCircle c α) : IncidenceGeometry.length a b = IncidenceGeometry.length a c

theorem SyntheticEuclid4.on_circle_of_oncircle_length [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {α : IncidenceGeometry.Circle} (aα : IncidenceGeometry.CenterCircle a α) (bα : IncidenceGeometry.OnCircle b α) (ab_ac : IncidenceGeometry.length a b ≠ IncidenceGeometry.length a c) : ¬IncidenceGeometry.OnCircle c α

theorem SyntheticEuclid4.incircle_of_on_circle_length [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {α : IncidenceGeometry.Circle} (aα : IncidenceGeometry.CenterCircle a α) (bα : IncidenceGeometry.OnCircle b α) (ab_ac : IncidenceGeometry.length a b ≤ IncidenceGeometry.length a c) : ¬IncidenceGeometry.InCircle c α

theorem SyntheticEuclid4.length_eq_of_B_B [I : IncidenceGeometry] {a b d e f : IncidenceGeometry.Point} (Bdbe : IncidenceGeometry.B d b e) (Bdaf : IncidenceGeometry.B d a f) (da_db : IncidenceGeometry.length d a = IncidenceGeometry.length d b) (de_df : IncidenceGeometry.length d e = IncidenceGeometry.length d f) : IncidenceGeometry.length a f = IncidenceGeometry.length b e

theorem SyntheticEuclid4.B_oncircle_of_inside_outside [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {α : IncidenceGeometry.Circle} (a_in_α : IncidenceGeometry.InCircle a α) (b_out_α : outCircle b α) : ∃ (c : IncidenceGeometry.Point), IncidenceGeometry.B a c b ∧ IncidenceGeometry.OnCircle c α

theorem SyntheticEuclid4.out_circle_of_lt [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {α : IncidenceGeometry.Circle} (aα : IncidenceGeometry.CenterCircle a α) (bα : IncidenceGeometry.OnCircle b α) (ab_lt_ac : IncidenceGeometry.length a b < IncidenceGeometry.length a c) : outCircle c α

theorem SyntheticEuclid4.sss [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} (ab_de : IncidenceGeometry.length a b = IncidenceGeometry.length d e) (bc_ef : IncidenceGeometry.length b c = IncidenceGeometry.length e f) (ac_df : IncidenceGeometry.length a c = IncidenceGeometry.length d f) : IncidenceGeometry.angle a b c = IncidenceGeometry.angle d e f ∧ IncidenceGeometry.angle b a c = IncidenceGeometry.angle e d f ∧ IncidenceGeometry.angle a c b = IncidenceGeometry.angle d f e

theorem SyntheticEuclid4.sas [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} (ab_de : IncidenceGeometry.length a b = IncidenceGeometry.length d e) (ac_df : IncidenceGeometry.length a c = IncidenceGeometry.length d f) (Abac : IncidenceGeometry.angle b a c = IncidenceGeometry.angle e d f) : IncidenceGeometry.length b c = IncidenceGeometry.length e f ∧ IncidenceGeometry.angle a b c = IncidenceGeometry.angle d e f ∧ IncidenceGeometry.angle a c b = IncidenceGeometry.angle d f e

theorem SyntheticEuclid4.tri132_of_tri123 [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri_abc : triangle a b c) : triangle a c b

theorem SyntheticEuclid4.tri231_of_tri123 [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri_abc : triangle a b c) : triangle b c a

theorem SyntheticEuclid4.tri312 [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri_abc : triangle a b c) : triangle c a b

theorem SyntheticEuclid4.tri213 [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri_abc : triangle a b c) : triangle b a c

theorem SyntheticEuclid4.tri321 [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri_abc : triangle a b c) : triangle c b a

theorem SyntheticEuclid4.area_eq_of_sas [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} (ab_de : IncidenceGeometry.length a b = IncidenceGeometry.length d e) (ac_df : IncidenceGeometry.length a c = IncidenceGeometry.length d f) (Abac_Aedf : IncidenceGeometry.angle b a c = IncidenceGeometry.angle e d f) : IncidenceGeometry.area a b c = IncidenceGeometry.area d e f

theorem SyntheticEuclid4.angle_extension_of_B [I : IncidenceGeometry] {a b b1 c : IncidenceGeometry.Point} (ac : a ≠ c) (Babb1 : IncidenceGeometry.B a b b1) : IncidenceGeometry.angle b a c = IncidenceGeometry.angle b1 a c

theorem SyntheticEuclid4.area_add_of_B [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} (Babc : IncidenceGeometry.B a b c) (tri_dac : triangle d a c) : IncidenceGeometry.area d a b + IncidenceGeometry.area d c b = IncidenceGeometry.area d a c

theorem SyntheticEuclid4.area_add_of_B_offline [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (aL : IncidenceGeometry.OnLine a L) (cL : IncidenceGeometry.OnLine c L) (dL : ¬IncidenceGeometry.OnLine d L) : IncidenceGeometry.area d a b + IncidenceGeometry.area d c b = IncidenceGeometry.area d a c

theorem SyntheticEuclid4.col_of_area_zero_ne [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (ab : a ≠ b) (area_abc : IncidenceGeometry.area a b c = 0) : colinear a b c

theorem SyntheticEuclid4.col_132_of_col [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (col_123 : colinear a b c) : colinear a c b

theorem SyntheticEuclid4.col_213_of_col [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (col_123 : colinear a b c) : colinear b a c

theorem SyntheticEuclid4.col_312 [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (col : colinear a b c) : colinear c a b

theorem SyntheticEuclid4.col_134_of_col_123_col_124 [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} (ab : a ≠ b) (col_123 : colinear a b c) (col_124 : colinear a b d) : colinear a c d

theorem SyntheticEuclid4.tri_143_of_tri_col [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} (ad : a ≠ d) (tri_abc : triangle a b c) (col_abd : colinear a b d) : triangle a d c

theorem SyntheticEuclid4.col_of_B [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (Babc : IncidenceGeometry.B a b c) : colinear a b c

theorem SyntheticEuclid4.pt_inter_of_not_sameside [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (abL : ¬IncidenceGeometry.SameSide a b L) : ∃ (c : IncidenceGeometry.Point) (M : IncidenceGeometry.Line), IncidenceGeometry.OnLine a M ∧ IncidenceGeometry.OnLine b M ∧ IncidenceGeometry.OnLine c M ∧ IncidenceGeometry.OnLine c L

theorem SyntheticEuclid4.ne_of_diffside [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (abL : diffside a b L) : a ≠ b

theorem SyntheticEuclid4.ne_of_online [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (aL : IncidenceGeometry.OnLine a L) (bL : ¬IncidenceGeometry.OnLine b L) : a ≠ b

theorem SyntheticEuclid4.ne_of_online' [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (aL : IncidenceGeometry.OnLine a L) (bL : ¬IncidenceGeometry.OnLine b L) : b ≠ a

theorem SyntheticEuclid4.ne_line_of_online [I : IncidenceGeometry] {b : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (bM : IncidenceGeometry.OnLine b M) (bL : ¬IncidenceGeometry.OnLine b L) : L ≠ M

theorem SyntheticEuclid4.ne_line_of_online' [I : IncidenceGeometry] {b : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (bM : IncidenceGeometry.OnLine b M) (bL : ¬IncidenceGeometry.OnLine b L) : M ≠ L

theorem SyntheticEuclid4.pt_B_of_diffside [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (abL : diffside a b L) : ∃ (c : IncidenceGeometry.Point), IncidenceGeometry.OnLine c L ∧ IncidenceGeometry.B a c b

theorem SyntheticEuclid4.B_of_three_col_ne [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (ab : a ≠ b) (ac : a ≠ c) (bc : b ≠ c) (col_abc : colinear a b c) : IncidenceGeometry.B a b c ∨ IncidenceGeometry.B b a c ∨ IncidenceGeometry.B a c b

theorem SyntheticEuclid4.B_of_length_eq_col [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (ab : a ≠ b) (ac : a ≠ c) (col_abc : colinear a b c) (ab_cb : IncidenceGeometry.length a b = IncidenceGeometry.length c b) : IncidenceGeometry.B a b c

theorem SyntheticEuclid4.length_zero_of_eq [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} (ab : a = b) : IncidenceGeometry.length a b = 0

theorem SyntheticEuclid4.eq_of_length_zero [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} (ab_0 : IncidenceGeometry.length a b = 0) : a = b

theorem SyntheticEuclid4.ne_of_triangle_length_eq [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} (tri_abc : triangle a b c) (bd_cd : IncidenceGeometry.length b d = IncidenceGeometry.length c d) : b ≠ d

theorem SyntheticEuclid4.angle_extension_of_B' [I : IncidenceGeometry] {a b b1 c : IncidenceGeometry.Point} (ac : a ≠ c) (Babb1 : IncidenceGeometry.B a b b1) : IncidenceGeometry.angle c a b = IncidenceGeometry.angle c a b1

theorem SyntheticEuclid4.online_of_B_online [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (aL : IncidenceGeometry.OnLine a L) (cL : ¬IncidenceGeometry.OnLine c L) : ¬IncidenceGeometry.OnLine b L

theorem SyntheticEuclid4.online_of_B_online' [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (bL : IncidenceGeometry.OnLine b L) (cL : ¬IncidenceGeometry.OnLine c L) : ¬IncidenceGeometry.OnLine a L

theorem SyntheticEuclid4.online_of_B_online'' [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (aL : IncidenceGeometry.OnLine a L) (bL : ¬IncidenceGeometry.OnLine b L) : ¬IncidenceGeometry.OnLine c L

theorem SyntheticEuclid4.sameside_of_B_online_3 [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (aL : IncidenceGeometry.OnLine a L) (cL : ¬IncidenceGeometry.OnLine c L) : IncidenceGeometry.SameSide b c L

theorem SyntheticEuclid4.ne_of_sameside [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (bL : IncidenceGeometry.OnLine b L) (acL : IncidenceGeometry.SameSide a c L) : a ≠ b

theorem SyntheticEuclid4.ne_of_sameside' [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (cL : IncidenceGeometry.OnLine c L) (abL : IncidenceGeometry.SameSide a b L) : c ≠ a

theorem SyntheticEuclid4.tri_of_B_B_tri [I : IncidenceGeometry] {a b c d e : IncidenceGeometry.Point} (Babd : IncidenceGeometry.B a b d) (Bace : IncidenceGeometry.B a c e) (tri_abc : triangle a b c) : triangle a d e

theorem SyntheticEuclid4.ne_21_of_B [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (Babc : IncidenceGeometry.B a b c) : b ≠ a

theorem SyntheticEuclid4.ne_32_of_B [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (Babc : IncidenceGeometry.B a b c) : c ≠ b

theorem SyntheticEuclid4.ne_31_of_B [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (Babc : IncidenceGeometry.B a b c) : c ≠ a

theorem SyntheticEuclid4.sameside_or_of_diffside' [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (cL : ¬IncidenceGeometry.OnLine c L) (abL : diffside a b L) : IncidenceGeometry.SameSide a c L ∨ IncidenceGeometry.SameSide b c L

theorem SyntheticEuclid4.rightangle_of_angle_eq [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (aL : IncidenceGeometry.OnLine a L) (cL : IncidenceGeometry.OnLine c L) (dL : ¬IncidenceGeometry.OnLine d L) (dba_dbc : IncidenceGeometry.angle d b a = IncidenceGeometry.angle d b c) : IncidenceGeometry.angle d b a = IncidenceGeometry.rightangle ∧ IncidenceGeometry.angle d b c = IncidenceGeometry.rightangle

theorem SyntheticEuclid4.diffside_of_not_online' [I : IncidenceGeometry] {a : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (aL : ¬IncidenceGeometry.OnLine a L) : ∃ (b : IncidenceGeometry.Point), diffside a b L

theorem SyntheticEuclid4.pts_line_circle_of_not_sameside [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} {α : IncidenceGeometry.Circle} (aα : IncidenceGeometry.CenterCircle a α) (bα : IncidenceGeometry.OnCircle b α) (abL : ¬IncidenceGeometry.SameSide a b L) : ∃ (c : IncidenceGeometry.Point) (d : IncidenceGeometry.Point), c ≠ d ∧ IncidenceGeometry.OnLine c L ∧ IncidenceGeometry.OnLine d L ∧ IncidenceGeometry.OnCircle c α ∧ IncidenceGeometry.OnCircle d α

theorem SyntheticEuclid4.B_or_B_of_B_B [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} (cd : c ≠ d) (Babc : IncidenceGeometry.B a b c) (Babd : IncidenceGeometry.B a b d) : IncidenceGeometry.B b c d ∨ IncidenceGeometry.B b d c

theorem SyntheticEuclid4.angle_extension_of_B_B [I : IncidenceGeometry] {a b c d e : IncidenceGeometry.Point} (be : b ≠ e) (Babc : IncidenceGeometry.B a b c) (Babd : IncidenceGeometry.B a b d) : IncidenceGeometry.angle e b d = IncidenceGeometry.angle e b c

theorem SyntheticEuclid4.online_of_sameside_inter [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (ab : a ≠ b) (aL : IncidenceGeometry.OnLine a L) (aM : IncidenceGeometry.OnLine a M) (bL : IncidenceGeometry.OnLine b L) (cM : IncidenceGeometry.OnLine c M) (cdL : IncidenceGeometry.SameSide c d L) : ¬IncidenceGeometry.OnLine b M

theorem SyntheticEuclid4.diffside_of_sameside_sameside [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (aL : IncidenceGeometry.OnLine a L) (aM : IncidenceGeometry.OnLine a M) (aN : IncidenceGeometry.OnLine a N) (bL : IncidenceGeometry.OnLine b L) (cM : IncidenceGeometry.OnLine c M) (dN : IncidenceGeometry.OnLine d N) (dcL : IncidenceGeometry.SameSide d c L) (bcN : IncidenceGeometry.SameSide b c N) : diffside b d M

theorem SyntheticEuclid4.angle_add_of_sameside [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (aM : IncidenceGeometry.OnLine a M) (cM : IncidenceGeometry.OnLine c M) (cdL : IncidenceGeometry.SameSide c d L) (bdM : IncidenceGeometry.SameSide b d M) : IncidenceGeometry.angle b a c = IncidenceGeometry.angle d a b + IncidenceGeometry.angle d a c

theorem SyntheticEuclid4.offline_of_B_offline [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L N : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (bN : IncidenceGeometry.OnLine b N) (dN : IncidenceGeometry.OnLine d N) (dL : ¬IncidenceGeometry.OnLine d L) : ¬IncidenceGeometry.OnLine a N

theorem SyntheticEuclid4.diffside_of_B_offline [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L N : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (bN : IncidenceGeometry.OnLine b N) (dN : IncidenceGeometry.OnLine d N) (dL : ¬IncidenceGeometry.OnLine d L) : diffside a c N

theorem SyntheticEuclid4.diffside_of_B_offline'' [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {N : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (aN : ¬IncidenceGeometry.OnLine a N) (bN : IncidenceGeometry.OnLine b N) : diffside a c N

theorem SyntheticEuclid4.sameside_of_B_sameside_sameside [I : IncidenceGeometry] {a b c d e : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (bL : IncidenceGeometry.OnLine b L) (bM : IncidenceGeometry.OnLine b M) (bN : IncidenceGeometry.OnLine b N) (aL : IncidenceGeometry.OnLine a L) (eM : IncidenceGeometry.OnLine e M) (dN : IncidenceGeometry.OnLine d N) (edL : IncidenceGeometry.SameSide e d L) (cdM : IncidenceGeometry.SameSide c d M) : IncidenceGeometry.SameSide a e N

theorem SyntheticEuclid4.B_or_B_of_sameside [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (bc : b ≠ c) (aL : IncidenceGeometry.OnLine a L) (col : colinear a b c) (bcL : IncidenceGeometry.SameSide b c L) : IncidenceGeometry.B a b c ∨ IncidenceGeometry.B a c b

theorem SyntheticEuclid4.angle_extension_of_sameside [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (ab : a ≠ b) (bL : IncidenceGeometry.OnLine b L) (col : colinear b c d) (cdL : IncidenceGeometry.SameSide c d L) : IncidenceGeometry.angle c b a = IncidenceGeometry.angle d b a

theorem SyntheticEuclid4.sameside_of_B_diffside_sameside [I : IncidenceGeometry] {a b c d e : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (bM : IncidenceGeometry.OnLine b M) (eM : IncidenceGeometry.OnLine e M) (dM : ¬IncidenceGeometry.OnLine d M) (edL : IncidenceGeometry.SameSide e d L) (cdM : ¬IncidenceGeometry.SameSide c d M) : IncidenceGeometry.SameSide a d M

theorem SyntheticEuclid4.offline_of_online_offline [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (bc : b ≠ c) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (bM : IncidenceGeometry.OnLine b M) (cM : IncidenceGeometry.OnLine c M) (aM : ¬IncidenceGeometry.OnLine a M) : ¬IncidenceGeometry.OnLine c L

theorem SyntheticEuclid4.offline_of_ne_online_offline [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (ab : a ≠ b) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (aM : IncidenceGeometry.OnLine a M) (cM : IncidenceGeometry.OnLine c M) (cL : ¬IncidenceGeometry.OnLine c L) : ¬IncidenceGeometry.OnLine b M

theorem SyntheticEuclid4.online_of_angle_zero [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (ab : a ≠ b) (ac : a ≠ c) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (bac_0 : IncidenceGeometry.angle b a c = 0) : IncidenceGeometry.OnLine c L ∧ ¬IncidenceGeometry.B b a c

theorem SyntheticEuclid4.B_of_col_diffside [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (col_abc : colinear a b c) (bL : IncidenceGeometry.OnLine b L) (acL : diffside a c L) : IncidenceGeometry.B a b c

theorem SyntheticEuclid4.B_of_col_sameside [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (bL : IncidenceGeometry.OnLine b L) (acL : IncidenceGeometry.SameSide a c L) : ¬IncidenceGeometry.B a b c

theorem SyntheticEuclid4.angle_zero_of_online [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (ab : a ≠ b) (ac : a ≠ c) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (cL : IncidenceGeometry.OnLine c L) (Bbac : ¬IncidenceGeometry.B b a c) : IncidenceGeometry.angle b a c = 0

theorem SyntheticEuclid4.sameside_of_B_diffside [I : IncidenceGeometry] {a b c e : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (bL : IncidenceGeometry.OnLine b L) (aeL : diffside a e L) : IncidenceGeometry.SameSide e c L

theorem SyntheticEuclid4.angle_zero_of_lt_eq [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (ab : a ≠ b) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (dcL : IncidenceGeometry.SameSide d c L) (bad_bac : IncidenceGeometry.angle b a d = IncidenceGeometry.angle b a c) : IncidenceGeometry.angle c a d = 0

Lemma for I.14 that handles some casework. If one angle is contained in another and are equal then a sub-angle is zero

theorem SyntheticEuclid4.angle_zero_of_lt_eq_B [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} (ab : a ≠ b) (Bbcd : IncidenceGeometry.B b c d) (tri_bad : triangle b a d) (bad_bac : IncidenceGeometry.angle b a d = IncidenceGeometry.angle b a c) : IncidenceGeometry.angle c a d = 0

theorem SyntheticEuclid4.ne_of_col_tri [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} (col_abc : colinear a b c) (tri_acd : triangle d a c) : d ≠ b

theorem SyntheticEuclid4.ne_of_col_tri' [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} (col_abc : colinear a b c) (tri_acd : triangle d a c) : b ≠ d

theorem SyntheticEuclid4.tri_of_B_tri [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} (Babc : IncidenceGeometry.B a b c) (tri_acd : triangle d a c) : triangle d b c

theorem SyntheticEuclid4.diffside_of_B_offline' [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (bL : IncidenceGeometry.OnLine b L) (aL : ¬IncidenceGeometry.OnLine a L) : diffside a c L

theorem SyntheticEuclid4.tri_of_B_B_base_tri [I : IncidenceGeometry] {a b c d e : IncidenceGeometry.Point} (Bade : IncidenceGeometry.B a d e) (Bbdc : IncidenceGeometry.B b d c) (tri_abc : triangle a b c) : triangle a e b

theorem SyntheticEuclid4.offline_of_B_B_tri [I : IncidenceGeometry] {a b c d e : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (Bade : IncidenceGeometry.B a d e) (Bbdc : IncidenceGeometry.B b d c) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (tri_abc : triangle a b c) : ¬IncidenceGeometry.OnLine e L

theorem SyntheticEuclid4.nonzero_angle_of_offline [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (ab : a ≠ b) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (cL : ¬IncidenceGeometry.OnLine c L) : IncidenceGeometry.angle c a b ≠ 0

theorem SyntheticEuclid4.zero_lt_angle_of_offline [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (ab : a ≠ b) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (cL : ¬IncidenceGeometry.OnLine c L) : 0 < IncidenceGeometry.angle c a b

theorem SyntheticEuclid4.zero_lt_angle_of_tri [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri_abc : triangle a b c) : 0 < IncidenceGeometry.angle c a b

theorem SyntheticEuclid4.sameside_of_B_B [I : IncidenceGeometry] {a b c d e : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (Bade : IncidenceGeometry.B a d e) (bL : IncidenceGeometry.OnLine b L) (dL : IncidenceGeometry.OnLine d L) (aL : ¬IncidenceGeometry.OnLine a L) : IncidenceGeometry.SameSide c e L

theorem SyntheticEuclid4.angle_lt_of_B_tri [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} (Bcdb : IncidenceGeometry.B c d b) (tri_abc : triangle a b c) : IncidenceGeometry.angle c a d < IncidenceGeometry.angle c a b

theorem SyntheticEuclid4.ne_of_oncircle [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {α : IncidenceGeometry.Circle} (aα : IncidenceGeometry.OnCircle a α) (bα : ¬IncidenceGeometry.OnCircle b α) : a ≠ b

theorem SyntheticEuclid4.B_or_B_of_circ_pt [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {α : IncidenceGeometry.Circle} (ab : a ≠ b) (aα : IncidenceGeometry.CenterCircle a α) (bα : ¬IncidenceGeometry.OnCircle b α) : ∃ (c : IncidenceGeometry.Point), (IncidenceGeometry.B a c b ∨ IncidenceGeometry.B a b c) ∧ IncidenceGeometry.OnCircle c α

theorem SyntheticEuclid4.in_circle_of_lt_lt [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {α β : IncidenceGeometry.Circle} (aα : IncidenceGeometry.CenterCircle a α) (bβ : IncidenceGeometry.CenterCircle b β) (cα : IncidenceGeometry.OnCircle c α) (dβ : IncidenceGeometry.OnCircle d β) (lt_cen : |IncidenceGeometry.length a c - IncidenceGeometry.length b d| < IncidenceGeometry.length a b) (cen_lt : IncidenceGeometry.length a b < IncidenceGeometry.length a c + IncidenceGeometry.length b d) : ∃ (e : IncidenceGeometry.Point), IncidenceGeometry.OnCircle e α ∧ IncidenceGeometry.InCircle e β

theorem SyntheticEuclid4.circint_of_lt_lt [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {α β : IncidenceGeometry.Circle} (aα : IncidenceGeometry.CenterCircle a α) (bβ : IncidenceGeometry.CenterCircle b β) (cα : IncidenceGeometry.OnCircle c α) (dβ : IncidenceGeometry.OnCircle d β) (lt_cen : |IncidenceGeometry.length a c - IncidenceGeometry.length b d| < IncidenceGeometry.length a b) (cen_lt : IncidenceGeometry.length a b < IncidenceGeometry.length a c + IncidenceGeometry.length b d) : IncidenceGeometry.CirclesInter α β

theorem SyntheticEuclid4.ang_2_nonzero_of_tri [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri_abc : triangle a b c) : IncidenceGeometry.angle b a c ≠ 0

theorem SyntheticEuclid4.not_B_symm [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (Babc : ¬IncidenceGeometry.B a b c) : ¬IncidenceGeometry.B c b a

theorem SyntheticEuclid4.ang_121_zero_of_ne [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} (ab : a ≠ b) : IncidenceGeometry.angle a b a = 0

theorem SyntheticEuclid4.ne_23_of_sa [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} (tri_abc : triangle a b c) (ab_de : IncidenceGeometry.length a b = IncidenceGeometry.length d e) (bac_edf : IncidenceGeometry.angle b a c = IncidenceGeometry.angle e d f) : e ≠ f

theorem SyntheticEuclid4.ne_23_of_sa' [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} (tri_abc : triangle a b c) (ac_df : IncidenceGeometry.length a c = IncidenceGeometry.length d f) (bac_edf : IncidenceGeometry.angle b a c = IncidenceGeometry.angle e d f) : e ≠ f

theorem SyntheticEuclid4.not_B_of_tri_ang [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} (tri_abc : triangle a b c) (ef : e ≠ f) (de : d ≠ e) (abc_def : IncidenceGeometry.angle a b c = IncidenceGeometry.angle d e f) : ¬IncidenceGeometry.B e d f

theorem SyntheticEuclid4.triangle_of_asa [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} (tri_abc : triangle a b c) (ab_de : IncidenceGeometry.length a b = IncidenceGeometry.length d e) (bac_edf : IncidenceGeometry.angle b a c = IncidenceGeometry.angle e d f) (abc_def : IncidenceGeometry.angle a b c = IncidenceGeometry.angle d e f) : triangle d e f

theorem SyntheticEuclid4.triangle_of_saa [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} (de : d ≠ e) (tri_abc : triangle a b c) (ac_df : IncidenceGeometry.length a c = IncidenceGeometry.length d f) (bac_edf : IncidenceGeometry.angle b a c = IncidenceGeometry.angle e d f) (abc_def : IncidenceGeometry.angle a b c = IncidenceGeometry.angle d e f) : triangle d e f

theorem SyntheticEuclid4.offline_of_online_inter [I : IncidenceGeometry] {a b c d e : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (bc : b ≠ c) (aM : IncidenceGeometry.OnLine a M) (bM : IncidenceGeometry.OnLine b M) (bL : IncidenceGeometry.OnLine b L) (cL : IncidenceGeometry.OnLine c L) (cN : IncidenceGeometry.OnLine c N) (dN : IncidenceGeometry.OnLine d N) (aL : ¬IncidenceGeometry.OnLine a L) (dL : ¬IncidenceGeometry.OnLine d L) (eM : IncidenceGeometry.OnLine e M) (eN : IncidenceGeometry.OnLine e N) : ¬IncidenceGeometry.OnLine e L

theorem SyntheticEuclid4.para_symm [I : IncidenceGeometry] {M N : IncidenceGeometry.Line} (paraMN : para M N) : para N M

theorem SyntheticEuclid4.offline_of_para [I : IncidenceGeometry] {a : IncidenceGeometry.Point} {M N : IncidenceGeometry.Line} (aM : IncidenceGeometry.OnLine a M) (paraMN : para M N) : ¬IncidenceGeometry.OnLine a N

theorem SyntheticEuclid4.offline_of_para' [I : IncidenceGeometry] {a : IncidenceGeometry.Point} {M N : IncidenceGeometry.Line} (aN : IncidenceGeometry.OnLine a N) (paraMN : para M N) : ¬IncidenceGeometry.OnLine a M

theorem SyntheticEuclid4.ne_of_para [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {M N : IncidenceGeometry.Line} (aM : IncidenceGeometry.OnLine a M) (bN : IncidenceGeometry.OnLine b N) (paraMN : para M N) : a ≠ b

theorem SyntheticEuclid4.ne_of_para' [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {M N : IncidenceGeometry.Line} (aM : IncidenceGeometry.OnLine a M) (bN : IncidenceGeometry.OnLine b N) (paraMN : para M N) : b ≠ a

theorem SyntheticEuclid4.not_para_of_inter [I : IncidenceGeometry] {a : IncidenceGeometry.Point} {M N : IncidenceGeometry.Line} (aM : IncidenceGeometry.OnLine a M) (aN : IncidenceGeometry.OnLine a N) : ¬para M N

theorem SyntheticEuclid4.diffside_of_B_sameside [I : IncidenceGeometry] {a c d e : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (Bcad : IncidenceGeometry.B c a d) (aL : IncidenceGeometry.OnLine a L) (ceL : IncidenceGeometry.SameSide c e L) : diffside d e L

theorem SyntheticEuclid4.pt_of_online_not_sameside [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (abM : ¬IncidenceGeometry.SameSide a b M) : ∃ (c : IncidenceGeometry.Point), IncidenceGeometry.OnLine c M ∧ IncidenceGeometry.OnLine c L

theorem SyntheticEuclid4.sameside_of_para_online [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {M N : IncidenceGeometry.Line} (aM : IncidenceGeometry.OnLine a M) (bM : IncidenceGeometry.OnLine b M) (paraMN : para M N) : IncidenceGeometry.SameSide a b N

theorem SyntheticEuclid4.sameside_of_para_online' [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} {M N : IncidenceGeometry.Line} (aN : IncidenceGeometry.OnLine a N) (bN : IncidenceGeometry.OnLine b N) (paraMN : para M N) : IncidenceGeometry.SameSide a b M

theorem SyntheticEuclid4.tri124_of_paragram [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {M N O P : IncidenceGeometry.Line} (pgram : paragram a b c d M N O P) : triangle a b d

theorem SyntheticEuclid4.sameside_of_sameside_diffside [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (aL : IncidenceGeometry.OnLine a L) (aM : IncidenceGeometry.OnLine a M) (aN : IncidenceGeometry.OnLine a N) (bL : IncidenceGeometry.OnLine b L) (cM : IncidenceGeometry.OnLine c M) (dN : IncidenceGeometry.OnLine d N) (cdL : IncidenceGeometry.SameSide c d L) (bdM : diffside b d M) : IncidenceGeometry.SameSide b c N

theorem SyntheticEuclid4.sameside_of_quad [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M N O : IncidenceGeometry.Line} (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (bM : IncidenceGeometry.OnLine b M) (cM : IncidenceGeometry.OnLine c M) (cN : IncidenceGeometry.OnLine c N) (dN : IncidenceGeometry.OnLine d N) (dO : IncidenceGeometry.OnLine d O) (aO : IncidenceGeometry.OnLine a O) (abN : IncidenceGeometry.SameSide a b N) (cdL : IncidenceGeometry.SameSide c d L) (adM : IncidenceGeometry.SameSide a d M) : IncidenceGeometry.SameSide b c O

theorem SyntheticEuclid4.diffside_of_paragram [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M N O P : IncidenceGeometry.Line} (bL : IncidenceGeometry.OnLine b L) (dL : IncidenceGeometry.OnLine d L) (pgram : paragram a b c d M N O P) : diffside a c L

theorem SyntheticEuclid4.offline_of_col_offline [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (bc : b ≠ c) (col_abc : colinear a b c) (bL : IncidenceGeometry.OnLine b L) (aL : ¬IncidenceGeometry.OnLine a L) : ¬IncidenceGeometry.OnLine c L

theorem SyntheticEuclid4.B_of_col_offline [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (bc : b ≠ c) (col_abc : colinear a b c) (bL : IncidenceGeometry.OnLine b L) (aL : ¬IncidenceGeometry.OnLine a L) (acL : ¬IncidenceGeometry.SameSide a c L) : IncidenceGeometry.B a b c

theorem SyntheticEuclid4.tri_of_sameside [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (bc : b ≠ c) (bL : IncidenceGeometry.OnLine b L) (cL : IncidenceGeometry.OnLine c L) (adL : IncidenceGeometry.SameSide a d L) : triangle a b c

theorem SyntheticEuclid4.B_diagonal_of_quad [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (bM : IncidenceGeometry.OnLine b M) (cM : IncidenceGeometry.OnLine c M) (cN : IncidenceGeometry.OnLine c N) (dN : IncidenceGeometry.OnLine d N) (abN : IncidenceGeometry.SameSide a b N) (cdL : IncidenceGeometry.SameSide c d L) (adM : IncidenceGeometry.SameSide a d M) : ∃ (e : IncidenceGeometry.Point) (P : IncidenceGeometry.Line) (O : IncidenceGeometry.Line), IncidenceGeometry.B b e d ∧ IncidenceGeometry.B a e c ∧ IncidenceGeometry.OnLine a P ∧ IncidenceGeometry.OnLine c P ∧ IncidenceGeometry.OnLine b O ∧ IncidenceGeometry.OnLine d O ∧ IncidenceGeometry.OnLine e P ∧ IncidenceGeometry.OnLine e O ∧ diffside b d P ∧ diffside a c O

theorem SyntheticEuclid4.quad_area_comm [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (bM : IncidenceGeometry.OnLine b M) (cM : IncidenceGeometry.OnLine c M) (cN : IncidenceGeometry.OnLine c N) (dN : IncidenceGeometry.OnLine d N) (abN : IncidenceGeometry.SameSide a b N) (cdL : IncidenceGeometry.SameSide c d L) (adM : IncidenceGeometry.SameSide a d M) : IncidenceGeometry.area a b d + IncidenceGeometry.area b c d = IncidenceGeometry.area a b c + IncidenceGeometry.area a c d

theorem SyntheticEuclid4.paragram_area_comm [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {M N O P : IncidenceGeometry.Line} (pgram : paragram a b c d M N O P) : IncidenceGeometry.area a b d + IncidenceGeometry.area b c d = IncidenceGeometry.area a b c + IncidenceGeometry.area a c d

theorem SyntheticEuclid4.sameside_of_not_B [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (bc : b ≠ c) (Babc : ¬IncidenceGeometry.B a b c) (bL : IncidenceGeometry.OnLine b L) (aL : ¬IncidenceGeometry.OnLine a L) (col_abc : colinear a b c) : IncidenceGeometry.SameSide a c L

theorem SyntheticEuclid4.diffside_of_diffside_para [I : IncidenceGeometry] {a b f : IncidenceGeometry.Point} {M O : IncidenceGeometry.Line} (aO : IncidenceGeometry.OnLine a O) (bO : IncidenceGeometry.OnLine b O) (afM : diffside a f M) (paraMO : para M O) : diffside b f M

theorem SyntheticEuclid4.diffside_of_B_para [I : IncidenceGeometry] {a c d f : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (Badf : IncidenceGeometry.B a d f) (aL : IncidenceGeometry.OnLine a L) (dL : IncidenceGeometry.OnLine d L) (dM : IncidenceGeometry.OnLine d M) (cM : IncidenceGeometry.OnLine c M) (cN : IncidenceGeometry.OnLine c N) (paraLN : para L N) : diffside a f M

theorem SyntheticEuclid4.diffside_of_B_pgram [I : IncidenceGeometry] {a b c d f : IncidenceGeometry.Point} {L M N O : IncidenceGeometry.Line} (Badf : IncidenceGeometry.B a d f) (pgram1 : paragram a d c b L M N O) : diffside b f M

theorem SyntheticEuclid4.sameside_of_B_pgram_pgram [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} {L M N O P Q : IncidenceGeometry.Line} (Badf : IncidenceGeometry.B a d f) (pgram1 : paragram a d c b L M N O) (pgram2 : paragram e f c b L P N Q) : IncidenceGeometry.SameSide b d P

theorem SyntheticEuclid4.sameside_of_B_prgram_pgram_trans [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} {L M N O P Q : IncidenceGeometry.Line} (Badf : IncidenceGeometry.B a d f) (pgram1 : paragram a d c b L M N O) (pgram2 : paragram e f c b L P N Q) : IncidenceGeometry.SameSide d e P

theorem SyntheticEuclid4.sameside_of_B_prgram_pgram_trans' [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} {L M N O P Q : IncidenceGeometry.Line} (Badf : IncidenceGeometry.B a d f) (pgram1 : paragram a d c b L M N O) (pgram2 : paragram e f c b L P N Q) : IncidenceGeometry.SameSide a e P

theorem SyntheticEuclid4.sameside_of_sameside_para [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {M N : IncidenceGeometry.Line} (aN : IncidenceGeometry.OnLine a N) (bN : IncidenceGeometry.OnLine b N) (acM : IncidenceGeometry.SameSide a c M) (paraMN : para M N) : IncidenceGeometry.SameSide b c M

theorem SyntheticEuclid4.diffside_of_sameside_paragram [I : IncidenceGeometry] {a b c d f : IncidenceGeometry.Point} {L M N O P : IncidenceGeometry.Line} (fL : IncidenceGeometry.OnLine f L) (cP : IncidenceGeometry.OnLine c P) (fP : IncidenceGeometry.OnLine f P) (afM : IncidenceGeometry.SameSide a f M) (pgram : paragram a b c d L M N O) : diffside b d P

theorem SyntheticEuclid4.diffside_of_sameside_2_paragram [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} {L M N O P Q : IncidenceGeometry.Line} (afM : IncidenceGeometry.SameSide a f M) (pgram1 : paragram a d c b L M N O) (pgram2 : paragram e f c b L P N Q) : diffside e d P

theorem SyntheticEuclid4.B_of_B_2_paragram [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} {L M N O P Q : IncidenceGeometry.Line} (df : d ≠ f) (Badf : ¬IncidenceGeometry.B a d f) (pgram1 : paragram a d c b L M N O) (pgram2 : paragram e f c b L P N Q) : IncidenceGeometry.B e f d

theorem SyntheticEuclid4.sameside_of_B_para [I : IncidenceGeometry] {a b e f : IncidenceGeometry.Point} {P Q : IncidenceGeometry.Line} (Bfea : IncidenceGeometry.B f e a) (fP : IncidenceGeometry.OnLine f P) (eQ : IncidenceGeometry.OnLine e Q) (bQ : IncidenceGeometry.OnLine b Q) (paraPQ : para P Q) : IncidenceGeometry.SameSide a b P

theorem SyntheticEuclid4.sameside_online_of_diffside [I : IncidenceGeometry] {a c d : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (dM : IncidenceGeometry.OnLine d M) (aM : IncidenceGeometry.OnLine a M) (aL : IncidenceGeometry.OnLine a L) (cdL : diffside c d L) : ∃ (b : IncidenceGeometry.Point), IncidenceGeometry.OnLine b M ∧ IncidenceGeometry.SameSide b c L

theorem SyntheticEuclid4.sameside_of_offline [I : IncidenceGeometry] {b c e : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (bL : IncidenceGeometry.OnLine b L) (cL : ¬IncidenceGeometry.OnLine c L) (bM : ¬IncidenceGeometry.OnLine b M) (eL : IncidenceGeometry.OnLine e L) (eM : IncidenceGeometry.OnLine e M) : ∃ (d : IncidenceGeometry.Point), IncidenceGeometry.OnLine d M ∧ IncidenceGeometry.SameSide d c L

theorem SyntheticEuclid4.angle_add_of_B [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (Bbcd : IncidenceGeometry.B b c d) (bL : IncidenceGeometry.OnLine b L) (cL : IncidenceGeometry.OnLine c L) (aL : ¬IncidenceGeometry.OnLine a L) : IncidenceGeometry.angle d a b = IncidenceGeometry.angle c a d + IncidenceGeometry.angle c a b

theorem SyntheticEuclid4.online_of_ne_ne [I : IncidenceGeometry] {a c : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (ac : a ≠ c) (LM : L ≠ M) (aL : IncidenceGeometry.OnLine a L) (cL : IncidenceGeometry.OnLine c L) (cM : IncidenceGeometry.OnLine c M) : ¬IncidenceGeometry.OnLine a M

theorem SyntheticEuclid4.sameside_of_B_sameside [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (Bbcd : IncidenceGeometry.B b c d) (dL : IncidenceGeometry.OnLine d L) (bL : ¬IncidenceGeometry.OnLine b L) (abL : IncidenceGeometry.SameSide a b L) : IncidenceGeometry.SameSide a c L

theorem SyntheticEuclid4.quad_add_of_quad [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (Bdef : IncidenceGeometry.B d e f) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (cM : IncidenceGeometry.OnLine c M) (fM : IncidenceGeometry.OnLine f M) (dN : IncidenceGeometry.OnLine d N) (eN : IncidenceGeometry.OnLine e N) (acN : IncidenceGeometry.SameSide a c N) (feL : IncidenceGeometry.SameSide f e L) (adM : IncidenceGeometry.SameSide a d M) : IncidenceGeometry.area a c f + IncidenceGeometry.area a f d = IncidenceGeometry.area a b e + IncidenceGeometry.area a e d + IncidenceGeometry.area b c e + IncidenceGeometry.area f e c

theorem SyntheticEuclid4.B_of_sq [I : IncidenceGeometry] {b c d e l x : IncidenceGeometry.Point} {L O P Q X : IncidenceGeometry.Line} (Bbxc : IncidenceGeometry.B b x c) (xX : IncidenceGeometry.OnLine x X) (lX : IncidenceGeometry.OnLine l X) (lP : IncidenceGeometry.OnLine l P) (paraQX : para Q X) (paraOX : para O X) (pgram : paragram b c d e L O P Q) : IncidenceGeometry.B e l d

theorem SyntheticEuclid4.sameside_of_pyth [I : IncidenceGeometry] {a b c d e l : IncidenceGeometry.Point} {L O P Q X : IncidenceGeometry.Line} (Beld : IncidenceGeometry.B e l d) (aX : IncidenceGeometry.OnLine a X) (lX : IncidenceGeometry.OnLine l X) (pgram : paragram b c d e L O P Q) (paraQX : para Q X) : IncidenceGeometry.SameSide a c Q

theorem SyntheticEuclid4.tri_tri_B_B_of_int [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (bL : IncidenceGeometry.OnLine b L) (cL : IncidenceGeometry.OnLine c L) (aM : IncidenceGeometry.OnLine a M) (cM : IncidenceGeometry.OnLine c M) (aN : IncidenceGeometry.OnLine a N) (bN : IncidenceGeometry.OnLine b N) (adL : IncidenceGeometry.SameSide a d L) (bdM : IncidenceGeometry.SameSide b d M) (cdN : IncidenceGeometry.SameSide c d N) : ∃ (e : IncidenceGeometry.Point), IncidenceGeometry.B a e c ∧ IncidenceGeometry.B b d e ∧ triangle a b e ∧ triangle c d e

theorem SyntheticEuclid4.line_circle_inter_sameside_of_offline [I : IncidenceGeometry] {a c : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} {α : IncidenceGeometry.Circle} (aL : IncidenceGeometry.OnLine a L) (aM : IncidenceGeometry.OnLine a M) (cM : IncidenceGeometry.OnLine c M) (cL : ¬IncidenceGeometry.OnLine c L) (aα : IncidenceGeometry.CenterCircle a α) : ∃ (d : IncidenceGeometry.Point), IncidenceGeometry.OnLine d M ∧ IncidenceGeometry.SameSide c d L ∧ IncidenceGeometry.OnCircle d α

theorem SyntheticEuclid4.len_eq_of_sameside [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (bc : b ≠ c) (aM : IncidenceGeometry.OnLine a M) (bM : IncidenceGeometry.OnLine b M) (bL : IncidenceGeometry.OnLine b L) (cL : IncidenceGeometry.OnLine c L) (aL : ¬IncidenceGeometry.OnLine a L) : ∃ (d : IncidenceGeometry.Point), IncidenceGeometry.OnLine d L ∧ IncidenceGeometry.SameSide c d M ∧ IncidenceGeometry.length a b = IncidenceGeometry.length b d

Euclid I.2, generalization

theorem SyntheticEuclid4.offLine_of_angle_lt [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L N : IncidenceGeometry.Line} (ad : a ≠ d) (dL : IncidenceGeometry.OnLine d L) (cN : IncidenceGeometry.OnLine c N) (dN : IncidenceGeometry.OnLine d N) (bcL : IncidenceGeometry.SameSide b c L) (adb_lt_adc : IncidenceGeometry.angle a d b < IncidenceGeometry.angle a d c) : ¬IncidenceGeometry.OnLine b N

theorem SyntheticEuclid4.sameside_of_B_not_online_3 [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (aL : IncidenceGeometry.OnLine a L) (cL : ¬IncidenceGeometry.OnLine c L) : IncidenceGeometry.SameSide b c L

theorem SyntheticEuclid4.sameside_of_sameside_sameside [I : IncidenceGeometry] {b c d e : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (dL : IncidenceGeometry.OnLine d L) (dM : IncidenceGeometry.OnLine d M) (dN : IncidenceGeometry.OnLine d N) (cN : IncidenceGeometry.OnLine c N) (eN : IncidenceGeometry.OnLine e N) (ceM : IncidenceGeometry.SameSide c e M) (bcL : IncidenceGeometry.SameSide b c L) : IncidenceGeometry.SameSide c e L

theorem SyntheticEuclid4.diffside_of_angle_lt [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (ad : a ≠ d) (dL : IncidenceGeometry.OnLine d L) (dM : IncidenceGeometry.OnLine d M) (dN : IncidenceGeometry.OnLine d N) (aL : IncidenceGeometry.OnLine a L) (bM : IncidenceGeometry.OnLine b M) (cN : IncidenceGeometry.OnLine c N) (aM : ¬IncidenceGeometry.OnLine a M) (bcL : IncidenceGeometry.SameSide b c L) (adb_lt_adc : IncidenceGeometry.angle a d b < IncidenceGeometry.angle a d c) : diffside a c M

theorem SyntheticEuclid4.online_sameside_diffside_len_ang_tri_of_ang_lt [I : IncidenceGeometry] {d e f h : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (tri_def : triangle d e f) (dL : IncidenceGeometry.OnLine d L) (eL : IncidenceGeometry.OnLine e L) (hM : IncidenceGeometry.OnLine h M) (dM : IncidenceGeometry.OnLine d M) (dN : IncidenceGeometry.OnLine d N) (fN : IncidenceGeometry.OnLine f N) (hfL : IncidenceGeometry.SameSide h f L) (edf_edh : IncidenceGeometry.angle e d f < IncidenceGeometry.angle e d h) : ∃ (g : IncidenceGeometry.Point), IncidenceGeometry.OnLine g M ∧ ¬IncidenceGeometry.OnLine f M ∧ IncidenceGeometry.SameSide h g L ∧ IncidenceGeometry.length f d = IncidenceGeometry.length d g ∧ IncidenceGeometry.angle h d e = IncidenceGeometry.angle g d e ∧ 0 < IncidenceGeometry.angle d g e ∧ triangle g d f ∧ diffside e g N

theorem SyntheticEuclid4.sameside_of_not_sameside_para [I : IncidenceGeometry] {b c e h : IncidenceGeometry.Point} {L N R S : IncidenceGeometry.Line} (bc : b ≠ c) (eh : e ≠ h) (eL : IncidenceGeometry.OnLine e L) (eR : IncidenceGeometry.OnLine e R) (eS : IncidenceGeometry.OnLine e S) (hL : IncidenceGeometry.OnLine h L) (cR : IncidenceGeometry.OnLine c R) (bS : IncidenceGeometry.OnLine b S) (bN : IncidenceGeometry.OnLine b N) (cN : IncidenceGeometry.OnLine c N) (bhR : ¬IncidenceGeometry.SameSide b h R) (paraLN : para L N) : IncidenceGeometry.SameSide c h S

theorem SyntheticEuclid4.not_para [I : IncidenceGeometry] {L M : IncidenceGeometry.Line} (paraLM : ¬para L M) : ∃ (a : IncidenceGeometry.Point), IncidenceGeometry.OnLine a L ∧ IncidenceGeometry.OnLine a M

theorem SyntheticEuclid4.tri_sum_contra [I : IncidenceGeometry] {b c d e : IncidenceGeometry.Point} {O : IncidenceGeometry.Line} (bO : IncidenceGeometry.OnLine b O) (dO : IncidenceGeometry.OnLine d O) (eO : IncidenceGeometry.OnLine e O) (cO : ¬IncidenceGeometry.OnLine c O) (ar : IncidenceGeometry.area b c d = IncidenceGeometry.area b c e) : ¬IncidenceGeometry.B b e d

area of a triangle cannot equal the area of its subtriangle

theorem SyntheticEuclid4.zero_lt_area_tri [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (ab : a ≠ b) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (cL : ¬IncidenceGeometry.OnLine c L) : 0 < IncidenceGeometry.area a b c

theorem SyntheticEuclid4.ne_of_para_para [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (ab : a ≠ b) (aM : IncidenceGeometry.OnLine a M) (aN : IncidenceGeometry.OnLine a N) (bN : IncidenceGeometry.OnLine b N) (cM : IncidenceGeometry.OnLine c M) (paraLM : para L M) (paraLN : ¬para L N) : b ≠ c

theorem SyntheticEuclid4.B_of_B_para [I : IncidenceGeometry] {a b c e k : IncidenceGeometry.Point} {M N : IncidenceGeometry.Line} (Bakc : IncidenceGeometry.B a k c) (col_aeb : colinear a e b) (bM : IncidenceGeometry.OnLine b M) (cM : IncidenceGeometry.OnLine c M) (eN : IncidenceGeometry.OnLine e N) (kN : IncidenceGeometry.OnLine k N) (aN : ¬IncidenceGeometry.OnLine a N) (paraMN : para M N) : IncidenceGeometry.B a e b

theorem SyntheticEuclid4.not_B_of_sameside [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (abL : IncidenceGeometry.SameSide a b L) (cL : IncidenceGeometry.OnLine c L) : ¬IncidenceGeometry.B a c b

theorem SyntheticEuclid4.B_of_B_para_para [I : IncidenceGeometry] {a b c d e : IncidenceGeometry.Point} {L M O P : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (aL : IncidenceGeometry.OnLine a L) (aM : IncidenceGeometry.OnLine a M) (bO : IncidenceGeometry.OnLine b O) (cP : IncidenceGeometry.OnLine c P) (dM : IncidenceGeometry.OnLine d M) (dO : IncidenceGeometry.OnLine d O) (eM : IncidenceGeometry.OnLine e M) (eP : IncidenceGeometry.OnLine e P) (paraPO : para P O) (paraPL : para P L) (paraOL : para O L) : IncidenceGeometry.B e d a

theorem SyntheticEuclid4.diffside_of_B_para_para [I : IncidenceGeometry] {b f g h k : IncidenceGeometry.Point} {L M P Q R S : IncidenceGeometry.Line} (Bfgh : IncidenceGeometry.B f g h) (bL : IncidenceGeometry.OnLine b L) (hQ : IncidenceGeometry.OnLine h Q) (hM : IncidenceGeometry.OnLine h M) (hS : IncidenceGeometry.OnLine h S) (gP : IncidenceGeometry.OnLine g P) (fR : IncidenceGeometry.OnLine f R) (bS : IncidenceGeometry.OnLine b S) (bP : IncidenceGeometry.OnLine b P) (kS : IncidenceGeometry.OnLine k S) (kR : IncidenceGeometry.OnLine k R) (paraPR : para P R) (paraMR : para M R) (paraPM : para P M) (paraQL : para Q L) : diffside h k L

theorem SyntheticEuclid4.diffside_of_B_B_para [I : IncidenceGeometry] {a b e f g h : IncidenceGeometry.Point} {L P Q R S : IncidenceGeometry.Line} (Babe : IncidenceGeometry.B a b e) (Bfgh : IncidenceGeometry.B f g h) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (hS : IncidenceGeometry.OnLine h S) (bS : IncidenceGeometry.OnLine b S) (bP : IncidenceGeometry.OnLine b P) (gP : IncidenceGeometry.OnLine g P) (eR : IncidenceGeometry.OnLine e R) (fR : IncidenceGeometry.OnLine f R) (fQ : IncidenceGeometry.OnLine f Q) (gQ : IncidenceGeometry.OnLine g Q) (paraPR : para P R) (paraQL : para Q L) : diffside a g S

theorem SyntheticEuclid4.B_of_B_B_para [I : IncidenceGeometry] {a b e f g h k : IncidenceGeometry.Point} {L M P Q R S : IncidenceGeometry.Line} (Babe : IncidenceGeometry.B a b e) (Bfgh : IncidenceGeometry.B f g h) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (hM : IncidenceGeometry.OnLine h M) (hS : IncidenceGeometry.OnLine h S) (hQ : IncidenceGeometry.OnLine h Q) (bS : IncidenceGeometry.OnLine b S) (bP : IncidenceGeometry.OnLine b P) (gP : IncidenceGeometry.OnLine g P) (eR : IncidenceGeometry.OnLine e R) (fR : IncidenceGeometry.OnLine f R) (fQ : IncidenceGeometry.OnLine f Q) (kS : IncidenceGeometry.OnLine k S) (kR : IncidenceGeometry.OnLine k R) (paraPR : para P R) (paraQL : para Q L) (paraPM : para P M) (paraMR : para M R) : IncidenceGeometry.B f e k

theorem SyntheticEuclid4.square_eq_of_length_eq [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M N O P Q R S : IncidenceGeometry.Line} {b' a' d' c' : IncidenceGeometry.Point} (sq1 : square a b b' a') (sq2 : square c d d' c') (_pgram1 : paragram a b b' a' L M N O) (_pgram2 : paragram c d d' c' P Q R S) (len_eq : IncidenceGeometry.length a b = IncidenceGeometry.length c d) : IncidenceGeometry.area a b a' + IncidenceGeometry.area a' b b' = IncidenceGeometry.area c d c' + IncidenceGeometry.area c' d d'

theorem SyntheticEuclid4.iseqtri_iseqtri_diffside_of_ne [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} (ab : a ≠ b) : ∃ (c : IncidenceGeometry.Point) (d : IncidenceGeometry.Point) (L : IncidenceGeometry.Line), IncidenceGeometry.OnLine a L ∧ IncidenceGeometry.OnLine b L ∧ diffside c d L ∧ eqTri a b c ∧ eqTri a b d

Euclid I.1, construction of two equilateral triangles

theorem SyntheticEuclid4.iseqtri_sameside_of_ne [I : IncidenceGeometry] {a b d : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (ab : a ≠ b) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (dL : ¬IncidenceGeometry.OnLine d L) : ∃ (c : IncidenceGeometry.Point), ¬IncidenceGeometry.OnLine c L ∧ IncidenceGeometry.SameSide c d L ∧ eqTri a b c

Euclid I.1, construction of an equilateral triangle on the sameside of a point

theorem SyntheticEuclid4.iseqtri_of_ne [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} (ab : a ≠ b) : ∃ (c : IncidenceGeometry.Point), eqTri a b c

Euclid I.1, construction of a single equilateral triangle

theorem SyntheticEuclid4.length_eq_of_ne [I : IncidenceGeometry] {b c : IncidenceGeometry.Point} (a : IncidenceGeometry.Point) (bc : b ≠ c) : ∃ (f : IncidenceGeometry.Point), IncidenceGeometry.length a f = IncidenceGeometry.length b c

Euclid I.2, collapsing compass

theorem SyntheticEuclid4.length_eq_B_of_ne [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (ab : a ≠ b) (bc : b ≠ c) : ∃ (d : IncidenceGeometry.Point), IncidenceGeometry.B a b d ∧ IncidenceGeometry.length b c = IncidenceGeometry.length b d

Euclid I.2, generalization

theorem SyntheticEuclid4.length_eq_B_of_ne_four [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} (ab : a ≠ b) (cd : c ≠ d) : ∃ (f : IncidenceGeometry.Point), IncidenceGeometry.B a b f ∧ IncidenceGeometry.length c d = IncidenceGeometry.length b f

Euclid I.2, generalization

theorem SyntheticEuclid4.length_eq_of_sameside [I : IncidenceGeometry] {a b d : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (aL : IncidenceGeometry.OnLine a L) (bL : ¬IncidenceGeometry.OnLine b L) (aM : ¬IncidenceGeometry.OnLine a M) (dL : IncidenceGeometry.OnLine d L) (dM : IncidenceGeometry.OnLine d M) : ∃ (e : IncidenceGeometry.Point), IncidenceGeometry.OnLine e M ∧ diffside e b L ∧ IncidenceGeometry.length e d = IncidenceGeometry.length a b

Euclid I.2, generalization

theorem SyntheticEuclid4.length_eq_of_sameside' [I : IncidenceGeometry] {a b d : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (aL : IncidenceGeometry.OnLine a L) (bL : ¬IncidenceGeometry.OnLine b L) (aM : ¬IncidenceGeometry.OnLine a M) (dL : IncidenceGeometry.OnLine d L) (dM : IncidenceGeometry.OnLine d M) : ∃ (e : IncidenceGeometry.Point), IncidenceGeometry.OnLine e M ∧ IncidenceGeometry.SameSide e b L ∧ IncidenceGeometry.length e d = IncidenceGeometry.length a b

Euclid I.2, generalization

theorem SyntheticEuclid4.B_length_eq_of_ne_lt [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} (cd : c ≠ d) (cd_lt_ab : IncidenceGeometry.length c d < IncidenceGeometry.length a b) : ∃ (f : IncidenceGeometry.Point), IncidenceGeometry.B a f b ∧ IncidenceGeometry.length a f = IncidenceGeometry.length c d

Euclid I.3, Moving a smaller segment on top of a larger one

theorem SyntheticEuclid4.angle_eq_of_iso [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (iso_abc : isoTri a b c) : IncidenceGeometry.angle a b c = IncidenceGeometry.angle a c b

Euclid I.5, (part 1), isosceles triangles have equal angles

theorem SyntheticEuclid4.iso_of_angle_eq [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri_abc : triangle a b c) (abc_eq_acb : IncidenceGeometry.angle a b c = IncidenceGeometry.angle a c b) : IncidenceGeometry.length a b = IncidenceGeometry.length a c

Euclid I.6, a triangle with equal angles is isosceles

theorem SyntheticEuclid4.bisect_segment [I : IncidenceGeometry] {a b : IncidenceGeometry.Point} (ab : a ≠ b) : ∃ (e : IncidenceGeometry.Point), IncidenceGeometry.B a e b ∧ IncidenceGeometry.length a e = IncidenceGeometry.length b e

Euclid I.10, bisecting a segment

theorem SyntheticEuclid4.bisect_angle_iso [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (aM : IncidenceGeometry.OnLine a M) (cM : IncidenceGeometry.OnLine c M) (iso_abc : isoTri a b c) : ∃ (d : IncidenceGeometry.Point), IncidenceGeometry.angle b a d = IncidenceGeometry.angle c a d ∧ IncidenceGeometry.SameSide d b M ∧ IncidenceGeometry.SameSide d c L

Euclid I.9 lemma, bisecting an angle in an isosceles triangle

theorem SyntheticEuclid4.bisect_angle [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (aM : IncidenceGeometry.OnLine a M) (cM : IncidenceGeometry.OnLine c M) (tri_abc : triangle a b c) : ∃ (f : IncidenceGeometry.Point), IncidenceGeometry.angle b a f = IncidenceGeometry.angle c a f ∧ IncidenceGeometry.SameSide f b M ∧ IncidenceGeometry.SameSide f c L

Euclid I.9 lemma, bisecting an angle

theorem SyntheticEuclid4.perpendicular_of_online [I : IncidenceGeometry] {a b c f : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (fL : ¬IncidenceGeometry.OnLine f L) : ∃ (e : IncidenceGeometry.Point), IncidenceGeometry.SameSide e f L ∧ IncidenceGeometry.angle e b a = IncidenceGeometry.rightangle ∧ IncidenceGeometry.angle e b c = IncidenceGeometry.rightangle

Euclid I.11, Obtaining perpendicular angles from a point on a line

theorem SyntheticEuclid4.perpendicular_of_online' [I : IncidenceGeometry] {a b f : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (ab : a ≠ b) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (fL : ¬IncidenceGeometry.OnLine f L) : ∃ (c : IncidenceGeometry.Point), IncidenceGeometry.SameSide c f L ∧ IncidenceGeometry.angle a b c = IncidenceGeometry.rightangle

Euclid I.11, Obtaining a perpendicular angle from a point on a line

theorem SyntheticEuclid4.perpendicular_of_online'' [I : IncidenceGeometry] {a b f : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (ab : a ≠ b) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (fL : ¬IncidenceGeometry.OnLine f L) : ∃ (c : IncidenceGeometry.Point), diffside c f L ∧ IncidenceGeometry.angle a b c = IncidenceGeometry.rightangle

Euclid I.11, Obtaining a perpendicular angle from a point on a line

theorem SyntheticEuclid4.perpendicular_of_not_online [I : IncidenceGeometry] {a : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (aL : ¬IncidenceGeometry.OnLine a L) : ∃ (c : IncidenceGeometry.Point) (d : IncidenceGeometry.Point) (e : IncidenceGeometry.Point), IncidenceGeometry.B c e d ∧ IncidenceGeometry.OnLine c L ∧ IncidenceGeometry.OnLine d L ∧ IncidenceGeometry.OnLine e L ∧ IncidenceGeometry.angle a e c = IncidenceGeometry.rightangle ∧ IncidenceGeometry.angle a e d = IncidenceGeometry.rightangle

Euclid I.12, Obtaining perpendicular angles from a point off a line

theorem SyntheticEuclid4.two_right_of_flat_angle [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (dL : ¬IncidenceGeometry.OnLine d L) : IncidenceGeometry.angle d b a + IncidenceGeometry.angle d b c = 2 * IncidenceGeometry.rightangle

Euclid I.13, A generalization of I.11. Instead of requiring the angles to be perpendicular, they can be arbitrary

theorem SyntheticEuclid4.right_of_online_right [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (bd : b ≠ d) (tri_abc : triangle a b c) (bL : IncidenceGeometry.OnLine b L) (cL : IncidenceGeometry.OnLine c L) (dL : IncidenceGeometry.OnLine d L) (abd : IncidenceGeometry.angle a b d = IncidenceGeometry.rightangle) : IncidenceGeometry.angle a b c = IncidenceGeometry.rightangle

Euclid I.13, a corollary if we know one of the angles to be right

theorem SyntheticEuclid4.flat_of_two_right_angle [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (bd : b ≠ d) (bL : IncidenceGeometry.OnLine b L) (dL : IncidenceGeometry.OnLine d L) (acL : diffside a c L) (two_ra : IncidenceGeometry.angle d b a + IncidenceGeometry.angle d b c = 2 * IncidenceGeometry.rightangle) : IncidenceGeometry.B a b c

Euclid I.14, the converse of I.13. If angles add to two right angles then you have betweeness

theorem SyntheticEuclid4.vertical_angle [I : IncidenceGeometry] {a b c d e : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (Bdbe : IncidenceGeometry.B d b e) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (dL : ¬IncidenceGeometry.OnLine d L) : IncidenceGeometry.angle a b d = IncidenceGeometry.angle c b e

Euclid I.15, vertical angles are equal

theorem SyntheticEuclid4.vertical_angle' [I : IncidenceGeometry] {a b c d e : IncidenceGeometry.Point} (Babc : IncidenceGeometry.B a b c) (Bdbe : IncidenceGeometry.B d b e) (col_abd : ¬colinear a b d) : IncidenceGeometry.angle a b d = IncidenceGeometry.angle c b e

Euclid I.15, vertical angles are equal

theorem SyntheticEuclid4.internal_lt_external [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} (Babc : IncidenceGeometry.B a b c) (tri_abd : triangle a b d) : IncidenceGeometry.angle b d a < IncidenceGeometry.angle d b c

Euclid I.16, external angles are greater than interior angles

theorem SyntheticEuclid4.internal_lt_external' [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} (Babc : IncidenceGeometry.B a b c) (tri_abd : triangle a b d) : IncidenceGeometry.angle b a d < IncidenceGeometry.angle d b c

Euclid I.16, external angles are greater than interior angles

theorem SyntheticEuclid4.two_ang_lt_two_right_of_tri [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri_abc : triangle a b c) : IncidenceGeometry.angle a b c + IncidenceGeometry.angle a c b < 2 * IncidenceGeometry.rightangle

Euclid I.17, Any two angles of a triangle sum to less than two right angles

theorem SyntheticEuclid4.ang_lt_obtuse_of_tri [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri_abc : triangle a b c) (right_lt_abc : IncidenceGeometry.rightangle < IncidenceGeometry.angle a b c) : IncidenceGeometry.angle b a c < IncidenceGeometry.angle a b c ∧ IncidenceGeometry.angle a c b < IncidenceGeometry.angle a b c

Euclid I.17 corollary, An obtuse angle in a triangle is bigger than the other two angles

theorem SyntheticEuclid4.ang_lt_of_len_lt [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri_abc : triangle a b c) (len_lt : IncidenceGeometry.length c a < IncidenceGeometry.length c b) : IncidenceGeometry.angle c b a < IncidenceGeometry.angle c a b

Euclid I.18, Opposite larger sides you have larger angles in a triangle

theorem SyntheticEuclid4.len_lt_of_ang_lt [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri_abc : triangle a b c) (ang_lt : IncidenceGeometry.angle c b a < IncidenceGeometry.angle c a b) : IncidenceGeometry.length c a < IncidenceGeometry.length c b

Euclid I.19, larger angles correspond to larger opposide sides in a triangle

theorem SyntheticEuclid4.len_lt_of_tri' [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri_abc : triangle a b c) : IncidenceGeometry.length a b < IncidenceGeometry.length a c + IncidenceGeometry.length b c

Euclid I.20, a triangle inequality

theorem SyntheticEuclid4.len_lt_of_tri [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri_abc : triangle a b c) : IncidenceGeometry.length a b < IncidenceGeometry.length a c + IncidenceGeometry.length b c ∧ IncidenceGeometry.length b c < IncidenceGeometry.length b a + IncidenceGeometry.length c a ∧ IncidenceGeometry.length c a < IncidenceGeometry.length c b + IncidenceGeometry.length a b

Euclid I.20, the triangle inequalities

theorem SyntheticEuclid4.angle_len_leq_of_tri_in_out [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (bL : IncidenceGeometry.OnLine b L) (cL : IncidenceGeometry.OnLine c L) (aM : IncidenceGeometry.OnLine a M) (cM : IncidenceGeometry.OnLine c M) (aN : IncidenceGeometry.OnLine a N) (bN : IncidenceGeometry.OnLine b N) (adL : IncidenceGeometry.SameSide a d L) (bdM : IncidenceGeometry.SameSide b d M) (cdN : IncidenceGeometry.SameSide c d N) : IncidenceGeometry.length b d + IncidenceGeometry.length c d < IncidenceGeometry.length a b + IncidenceGeometry.length a c ∧ IncidenceGeometry.angle b a c < IncidenceGeometry.angle b d c

Euclid I.21, with one triangle in another and sharing a base, the sum of the other two sides of the outer triangle is larger than that for the inner triangle, and the top angle of the outer triangle is smaller than that of the interior triangle

theorem SyntheticEuclid4.triangle_of_ineq [I : IncidenceGeometry] {a a1 a2 b b1 b2 f : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (fL : ¬IncidenceGeometry.OnLine f L) (ab_lt_a1a2_b1b2 : IncidenceGeometry.length a b < IncidenceGeometry.length a1 a2 + IncidenceGeometry.length b1 b2) (a1a2_lt_ab_b1b2 : IncidenceGeometry.length a1 a2 < IncidenceGeometry.length a b + IncidenceGeometry.length b1 b2) (b1b2_lt_a1a2_ab : IncidenceGeometry.length b1 b2 < IncidenceGeometry.length a1 a2 + IncidenceGeometry.length a b) : ∃ (e : IncidenceGeometry.Point), IncidenceGeometry.length a e = IncidenceGeometry.length a1 a2 ∧ IncidenceGeometry.length b e = IncidenceGeometry.length b1 b2 ∧ IncidenceGeometry.SameSide e f L

Euclid I.22, making a triangle with prescribed lengths

theorem SyntheticEuclid4.triangle_copy [I : IncidenceGeometry] {a b d e f g : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (tri_def : triangle d e f) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (gL : ¬IncidenceGeometry.OnLine g L) (ab_de : IncidenceGeometry.length a b = IncidenceGeometry.length d e) : ∃ (c : IncidenceGeometry.Point), IncidenceGeometry.length a c = IncidenceGeometry.length d f ∧ IncidenceGeometry.length b c = IncidenceGeometry.length e f ∧ IncidenceGeometry.SameSide c g L

Euclid I.22, corollary, if you are copying a triangle

theorem SyntheticEuclid4.angle_copy [I : IncidenceGeometry] {a b c d e j : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (ab : a ≠ b) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (jL : ¬IncidenceGeometry.OnLine j L) (tri_cde : triangle c d e) : ∃ (h : IncidenceGeometry.Point), IncidenceGeometry.angle h a b = IncidenceGeometry.angle e c d ∧ IncidenceGeometry.SameSide h j L

Euclid I.23, copying an angle

theorem SyntheticEuclid4.angle_copy' [I : IncidenceGeometry] {a b c d e j : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (ab : a ≠ b) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (jL : ¬IncidenceGeometry.OnLine j L) (tri_cde : triangle c d e) : ∃ (h : IncidenceGeometry.Point), IncidenceGeometry.angle h a b = IncidenceGeometry.angle e c d ∧ diffside h j L

Euclid I.23, copying an angle

theorem SyntheticEuclid4.sameside_of_len_lt_tri [I : IncidenceGeometry] {d e f g : IncidenceGeometry.Point} {N O : IncidenceGeometry.Line} (dN : IncidenceGeometry.OnLine d N) (fN : IncidenceGeometry.OnLine f N) (fO : IncidenceGeometry.OnLine f O) (gO : IncidenceGeometry.OnLine g O) (tri_def : triangle d e f) (tri_gdf : triangle g d f) (egN : diffside e g N) (ab_le_ac : IncidenceGeometry.length d e ≤ IncidenceGeometry.length d f) (tri_fge : ¬colinear f g e) (dgf_dfg : IncidenceGeometry.angle d g f = IncidenceGeometry.angle d f g) : IncidenceGeometry.SameSide d e O

theorem SyntheticEuclid4.opp_lt_of_ss_lt [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} (tri_abc : triangle a b c) (tri_def : triangle d e f) (ab_de : IncidenceGeometry.length a b = IncidenceGeometry.length d e) (ac_df : IncidenceGeometry.length a c = IncidenceGeometry.length d f) (edf_lt_bac : IncidenceGeometry.angle e d f < IncidenceGeometry.angle b a c) : IncidenceGeometry.length e f < IncidenceGeometry.length b c

Euclid I.24, If two triangles have two congruent sides, and the included angle of one is bigger than the other then the opposite side is also bigger than that of the other triangle

theorem SyntheticEuclid4.ang_lt_of_ss_lt [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} (tri_abc : triangle a b c) (tri_def : triangle d e f) (ab_de : IncidenceGeometry.length a b = IncidenceGeometry.length d e) (ac_df : IncidenceGeometry.length a c = IncidenceGeometry.length d f) (ef_bc : IncidenceGeometry.length e f < IncidenceGeometry.length b c) : IncidenceGeometry.angle e d f < IncidenceGeometry.angle b a c

Euclid I.25, the converse of I.24

theorem SyntheticEuclid4.asa' [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} (tri_abc : triangle a b c) (tri_def : triangle d e f) (ab_de : IncidenceGeometry.length a b = IncidenceGeometry.length d e) (bac_edf : IncidenceGeometry.angle b a c = IncidenceGeometry.angle e d f) (abc_def : IncidenceGeometry.angle a b c = IncidenceGeometry.angle d e f) : IncidenceGeometry.length a c = IncidenceGeometry.length d f ∧ IncidenceGeometry.length b c = IncidenceGeometry.length e f ∧ IncidenceGeometry.angle a c b = IncidenceGeometry.angle d f e

Euclid I.26, if two triangles have two corresponding angles equal and the included sides equal, then they are congruent

theorem SyntheticEuclid4.asa [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} (tri_abc : triangle a b c) (ab_de : IncidenceGeometry.length a b = IncidenceGeometry.length d e) (bac_edf : IncidenceGeometry.angle b a c = IncidenceGeometry.angle e d f) (abc_def : IncidenceGeometry.angle a b c = IncidenceGeometry.angle d e f) : IncidenceGeometry.length a c = IncidenceGeometry.length d f ∧ IncidenceGeometry.length b c = IncidenceGeometry.length e f ∧ IncidenceGeometry.angle a c b = IncidenceGeometry.angle d f e

Euclid I.26, if two triangles have two corresponding angles equal and the included sides equal, then they are congruent

theorem SyntheticEuclid4.saa' [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} (tri_abc : triangle a b c) (tri_def : triangle d e f) (ac_df : IncidenceGeometry.length a c = IncidenceGeometry.length d f) (bac_edf : IncidenceGeometry.angle b a c = IncidenceGeometry.angle e d f) (abc_def : IncidenceGeometry.angle a b c = IncidenceGeometry.angle d e f) : IncidenceGeometry.length a b = IncidenceGeometry.length d e ∧ IncidenceGeometry.length b c = IncidenceGeometry.length e f ∧ IncidenceGeometry.angle a c b = IncidenceGeometry.angle d f e

Euclid I.26, if two triangles have two corresponding angles equal and a non-included side equal, then they are congruent

theorem SyntheticEuclid4.saa [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} (de : d ≠ e) (tri_abc : triangle a b c) (ac_df : IncidenceGeometry.length a c = IncidenceGeometry.length d f) (bac_edf : IncidenceGeometry.angle b a c = IncidenceGeometry.angle e d f) (abc_def : IncidenceGeometry.angle a b c = IncidenceGeometry.angle d e f) : IncidenceGeometry.length a b = IncidenceGeometry.length d e ∧ IncidenceGeometry.length b c = IncidenceGeometry.length e f ∧ IncidenceGeometry.angle a c b = IncidenceGeometry.angle d f e

Euclid I.26, if two triangles have two corresponding angles equal and a non-included side equal, then they are congruent

theorem SyntheticEuclid4.para_of_ang_eq [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (bc : b ≠ c) (aM : IncidenceGeometry.OnLine a M) (bM : IncidenceGeometry.OnLine b M) (bL : IncidenceGeometry.OnLine b L) (cL : IncidenceGeometry.OnLine c L) (cN : IncidenceGeometry.OnLine c N) (dN : IncidenceGeometry.OnLine d N) (adL : diffside a d L) (cba_bcd : IncidenceGeometry.angle c b a = IncidenceGeometry.angle b c d) : para M N

Euclid I.27, if the alternate angles are equal, then the lines it formed from are parallel

theorem SyntheticEuclid4.para_of_ext_ang_eq [I : IncidenceGeometry] {b c d e f : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (Bebc : IncidenceGeometry.B e b c) (bM : IncidenceGeometry.OnLine b M) (fM : IncidenceGeometry.OnLine f M) (bL : IncidenceGeometry.OnLine b L) (cL : IncidenceGeometry.OnLine c L) (cN : IncidenceGeometry.OnLine c N) (dN : IncidenceGeometry.OnLine d N) (fdL : IncidenceGeometry.SameSide f d L) (ebf_bcd : IncidenceGeometry.angle e b f = IncidenceGeometry.angle b c d) : para M N

Euclid I.28 part 1, If the exterior angle is equal to the internal and opposite angle then we have parallel Lines

theorem SyntheticEuclid4.para_of_int_ang_sum [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (bc : b ≠ c) (aM : IncidenceGeometry.OnLine a M) (bM : IncidenceGeometry.OnLine b M) (bL : IncidenceGeometry.OnLine b L) (cL : IncidenceGeometry.OnLine c L) (cN : IncidenceGeometry.OnLine c N) (dN : IncidenceGeometry.OnLine d N) (adL : IncidenceGeometry.SameSide a d L) (abc_bcd : IncidenceGeometry.angle a b c + IncidenceGeometry.angle b c d = 2 * IncidenceGeometry.rightangle) : para M N

Euclid I.28 part 2, If the sum of the interior angles is equal to two right angles then we have parallel Lines

theorem SyntheticEuclid4.alternate_eq_of_para [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (aM : IncidenceGeometry.OnLine a M) (bM : IncidenceGeometry.OnLine b M) (bL : IncidenceGeometry.OnLine b L) (cL : IncidenceGeometry.OnLine c L) (cN : IncidenceGeometry.OnLine c N) (dN : IncidenceGeometry.OnLine d N) (adL : diffside a d L) (paraMN : para M N) : IncidenceGeometry.angle a b c = IncidenceGeometry.angle b c d

Euclid I.29, basic properties of alternate, exterior, and interior angles with parallel lines

theorem SyntheticEuclid4.interior_rightangles_of_para [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (aM : IncidenceGeometry.OnLine a M) (bM : IncidenceGeometry.OnLine b M) (bL : IncidenceGeometry.OnLine b L) (cL : IncidenceGeometry.OnLine c L) (cN : IncidenceGeometry.OnLine c N) (dN : IncidenceGeometry.OnLine d N) (adL : IncidenceGeometry.SameSide a d L) (paraMN : para M N) : IncidenceGeometry.angle a b c + IncidenceGeometry.angle b c d = 2 * IncidenceGeometry.rightangle

Euclid I.29, basic properties of alternate, exterior, and interior angles with parallel lines

theorem SyntheticEuclid4.correspond_of_para [I : IncidenceGeometry] {a b c d e : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (Babc : IncidenceGeometry.B a b c) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (bM : IncidenceGeometry.OnLine b M) (dM : IncidenceGeometry.OnLine d M) (cN : IncidenceGeometry.OnLine c N) (eN : IncidenceGeometry.OnLine e N) (deL : IncidenceGeometry.SameSide d e L) (paraMN : para M N) : IncidenceGeometry.angle a b d = IncidenceGeometry.angle b c e

Euclid I.29, corresponding angles are equal

theorem SyntheticEuclid4.right_of_para_right [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (aM : IncidenceGeometry.OnLine a M) (bM : IncidenceGeometry.OnLine b M) (bL : IncidenceGeometry.OnLine b L) (cL : IncidenceGeometry.OnLine c L) (cN : IncidenceGeometry.OnLine c N) (dN : IncidenceGeometry.OnLine d N) (aL : ¬IncidenceGeometry.OnLine a L) (dL : ¬IncidenceGeometry.OnLine d L) (bcd : IncidenceGeometry.angle b c d = IncidenceGeometry.rightangle) (paraMN : para M N) : IncidenceGeometry.angle a b c = IncidenceGeometry.rightangle

theorem SyntheticEuclid4.para_trans [I : IncidenceGeometry] {L M N : IncidenceGeometry.Line} (MN : M ≠ N) (paraLM : para L M) (paraLN : para L N) : para M N

Euclid I.30, transitivity of parallel lines

theorem SyntheticEuclid4.lines_inter_of_para [I : IncidenceGeometry] {a : IncidenceGeometry.Point} {L M N : IncidenceGeometry.Line} (LM : L ≠ M) (aL : IncidenceGeometry.OnLine a L) (aM : IncidenceGeometry.OnLine a M) (paraMN : para M N) : ∃ (b : IncidenceGeometry.Point), IncidenceGeometry.OnLine b L ∧ IncidenceGeometry.OnLine b N

Euclid I.30, a corollary, a contrapositive of sorts of I.30

theorem SyntheticEuclid4.para_of_offline [I : IncidenceGeometry] {a : IncidenceGeometry.Point} {M : IncidenceGeometry.Line} (aM : ¬IncidenceGeometry.OnLine a M) : ∃ (N : IncidenceGeometry.Line), IncidenceGeometry.OnLine a N ∧ para M N

Euclid I.31, through a point off a line there exists a parallel line

theorem SyntheticEuclid4.ext_int_sum_of_tri [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} (Bbcd : IncidenceGeometry.B b c d) (tri_abc : triangle a b c) : IncidenceGeometry.angle a c d = IncidenceGeometry.angle b a c + IncidenceGeometry.angle a b c ∧ IncidenceGeometry.angle a b c + IncidenceGeometry.angle b c a + IncidenceGeometry.angle c a b = 2 * IncidenceGeometry.rightangle

Euclid I.32, the exterior angle equals the sum of the other two angles and the sum of all three interior angles adds to two right angles

theorem SyntheticEuclid4.sum_two_right_of_tri [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri_abc : triangle a b c) : IncidenceGeometry.angle a b c + IncidenceGeometry.angle b c a + IncidenceGeometry.angle c a b = 2 * IncidenceGeometry.rightangle

theorem SyntheticEuclid4.pgram_of_para_len_eq [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M N O P : IncidenceGeometry.Line} (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (bO : IncidenceGeometry.OnLine b O) (dO : IncidenceGeometry.OnLine d O) (dM : IncidenceGeometry.OnLine d M) (cM : IncidenceGeometry.OnLine c M) (cN : IncidenceGeometry.OnLine c N) (aN : IncidenceGeometry.OnLine a N) (bP : IncidenceGeometry.OnLine b P) (cP : IncidenceGeometry.OnLine c P) (aPd : diffside a d P) (paraLM : para L M) (ab_cd : IncidenceGeometry.length a b = IncidenceGeometry.length c d) : paragram a b d c L O M N

Euclid I.33, parallel lines with pair of points with same length make a parallelogram

theorem SyntheticEuclid4.len_ang_area_eq_of_parallelogram [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {M N O P : IncidenceGeometry.Line} (pgram : paragram a b c d M N O P) : IncidenceGeometry.length a b = IncidenceGeometry.length c d ∧ IncidenceGeometry.angle b a d = IncidenceGeometry.angle b c d ∧ IncidenceGeometry.area a b d = IncidenceGeometry.area b c d

Euclid I.34, basic length, angle, and area properties of paralellograms

theorem SyntheticEuclid4.len_eq_of_parallelogram [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {M N O P : IncidenceGeometry.Line} (pgram : paragram a b c d M N O P) : IncidenceGeometry.length a b = IncidenceGeometry.length c d

Euclid I.34, basic length properties of paralellograms

theorem SyntheticEuclid4.len_eq_of_parallelogram' [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {M N O P : IncidenceGeometry.Line} (pgram : paragram a b c d M N O P) : IncidenceGeometry.length a d = IncidenceGeometry.length c b

Euclid I.34, basic length properties of paralellograms

theorem SyntheticEuclid4.area_eq_of_parallelogram [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {M N O P : IncidenceGeometry.Line} (pgram : paragram a b c d M N O P) : IncidenceGeometry.area a b d = IncidenceGeometry.area b c d

Euclid I.34, basic area properties of paralellograms

theorem SyntheticEuclid4.B_sameside_of_2_paragram [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} {L M N O P Q : IncidenceGeometry.Line} (Badf : IncidenceGeometry.B a d f) (pgram1 : paragram a d c b L M N O) (pgram2 : paragram e f c b L P N Q) : IncidenceGeometry.B f e a ∧ IncidenceGeometry.SameSide d e P

theorem SyntheticEuclid4.area_eq_of_paragram [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} {L M N O P Q : IncidenceGeometry.Line} (pgram1 : paragram a d c b L M N O) (pgram2 : paragram e f c b L P N Q) : IncidenceGeometry.area a d b + IncidenceGeometry.area d b c = IncidenceGeometry.area e f b + IncidenceGeometry.area f b c

Euclid I.35, parallelograms sharing two parallels have the same area

theorem SyntheticEuclid4.area_eq_of_far_paragram [I : IncidenceGeometry] {a b c d e f g h : IncidenceGeometry.Point} {L M N O P Q : IncidenceGeometry.Line} (pgram1 : paragram a d c b L M N O) (pgram2 : paragram e h g f L P N Q) (bc_fg : IncidenceGeometry.length b c = IncidenceGeometry.length f g) : IncidenceGeometry.area a d b + IncidenceGeometry.area d b c = IncidenceGeometry.area f g e + IncidenceGeometry.area g e h

Euclid I.36, generalization of I.35 to parallelograms with a distance

theorem SyntheticEuclid4.paragram_of_tri_para [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} {M N : IncidenceGeometry.Line} (bc : b ≠ c) (bM : IncidenceGeometry.OnLine b M) (cM : IncidenceGeometry.OnLine c M) (aN : IncidenceGeometry.OnLine a N) (paraMN : para M N) : ∃ (d : IncidenceGeometry.Point) (L : IncidenceGeometry.Line) (O : IncidenceGeometry.Line), paragram d a c b N L M O

Proof of the construction of the parallelogram from the triangle in I.37, used twice so worth having as its own lemma

theorem SyntheticEuclid4.area_eq_of_tri_far [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (aL : IncidenceGeometry.OnLine a L) (dL : IncidenceGeometry.OnLine d L) (bM : IncidenceGeometry.OnLine b M) (cM : IncidenceGeometry.OnLine c M) (eM : IncidenceGeometry.OnLine e M) (fM : IncidenceGeometry.OnLine f M) (bc_ef : IncidenceGeometry.length b c = IncidenceGeometry.length e f) (paraLM : para L M) : IncidenceGeometry.area a b c = IncidenceGeometry.area d e f

Euclid I.38, the analog of I.35 for triangles

theorem SyntheticEuclid4.area_eq_of_tri [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (aL : IncidenceGeometry.OnLine a L) (dL : IncidenceGeometry.OnLine d L) (bM : IncidenceGeometry.OnLine b M) (cM : IncidenceGeometry.OnLine c M) (paraLM : para L M) : IncidenceGeometry.area a b c = IncidenceGeometry.area d b c

Euclid I.37, triangles sharing two parallels have the same area

theorem SyntheticEuclid4.para_of_tri_sameside_area_far [I : IncidenceGeometry] {a b c d e f : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (ad : a ≠ d) (tri_abc : triangle a b c) (tri_def : triangle d e f) (bL : IncidenceGeometry.OnLine b L) (cL : IncidenceGeometry.OnLine c L) (eL : IncidenceGeometry.OnLine e L) (fL : IncidenceGeometry.OnLine f L) (aM : IncidenceGeometry.OnLine a M) (dM : IncidenceGeometry.OnLine d M) (adL : IncidenceGeometry.SameSide a d L) (bc_ef : IncidenceGeometry.length b c = IncidenceGeometry.length e f) (eqTri : IncidenceGeometry.area a b c = IncidenceGeometry.area d e f) : para L M

Euclid I.40, equal area triangles on the same side must be on the same parallels

theorem SyntheticEuclid4.para_of_tri_sameside_area [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M : IncidenceGeometry.Line} (ad : a ≠ d) (tri_abc : triangle a b c) (tri_dbc : triangle d b c) (bL : IncidenceGeometry.OnLine b L) (cL : IncidenceGeometry.OnLine c L) (aM : IncidenceGeometry.OnLine a M) (dM : IncidenceGeometry.OnLine d M) (adL : IncidenceGeometry.SameSide a d L) (eqTri : IncidenceGeometry.area a b c = IncidenceGeometry.area b c d) : para L M

Euclid I.39, equal area triangles on the same side must be on the same parallels

theorem SyntheticEuclid4.twice_pgram_of_tri [I : IncidenceGeometry] {a b c d e : IncidenceGeometry.Point} {L M N O : IncidenceGeometry.Line} (eL : IncidenceGeometry.OnLine e L) (pgram : paragram a b c d L M N O) : IncidenceGeometry.area a b d + IncidenceGeometry.area b c d = 2 * IncidenceGeometry.area c d e

Euclid I.41, if a parallelogram shares the same parallels as a triangle and the same base, then the parallelogram has twice the area of the triangle

theorem SyntheticEuclid4.pgram_of_angle_tri [I : IncidenceGeometry] {a b c d e f h i : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} {n : IncidenceGeometry.Point} (hi : h ≠ i) (tri_abc : triangle a b c) (tri_def : triangle d e f) (hL : IncidenceGeometry.OnLine h L) (iL : IncidenceGeometry.OnLine i L) (nL : ¬IncidenceGeometry.OnLine n L) : ∃ (j : IncidenceGeometry.Point) (l : IncidenceGeometry.Point) (m : IncidenceGeometry.Point) (M : IncidenceGeometry.Line) (N : IncidenceGeometry.Line) (O : IncidenceGeometry.Line), IncidenceGeometry.B h i j ∧ paragram m l i j N M L O ∧ IncidenceGeometry.area j i l + IncidenceGeometry.area l m j = IncidenceGeometry.area a b c ∧ IncidenceGeometry.SameSide n l L ∧ IncidenceGeometry.angle l i j = IncidenceGeometry.angle d e f

Euclid I.42, to construct a parallelogram with the area of a given triangle and with a given angle

theorem SyntheticEuclid4.pgram_complement_eq [I : IncidenceGeometry] {a b c d e f g h k : IncidenceGeometry.Point} {L M N O P Q : IncidenceGeometry.Line} (Bakc : IncidenceGeometry.B a k c) (hM : IncidenceGeometry.OnLine h M) (hQ : IncidenceGeometry.OnLine h Q) (fN : IncidenceGeometry.OnLine f N) (fP : IncidenceGeometry.OnLine f P) (pgram1 : paragram d a b c O L M N) (pgram2 : paragram g a e k O L P Q) : IncidenceGeometry.area k d g + IncidenceGeometry.area k d f = IncidenceGeometry.area k b e + IncidenceGeometry.area k b h

Euclid I.43, complementary parallelograms accross the diameter of a parallelogram are equal

theorem SyntheticEuclid4.lines_inter_of_pgram [I : IncidenceGeometry] {a b e f g h : IncidenceGeometry.Point} {L M P Q R S : IncidenceGeometry.Line} (Babe : IncidenceGeometry.B a b e) (Bfgh : IncidenceGeometry.B f g h) (pgram1 : paragram f g b e Q P L R) (pgram2 : paragram a b g h L P Q M) (bS : IncidenceGeometry.OnLine b S) (hS : IncidenceGeometry.OnLine h S) (paraMR : para M R) : ∃ (k : IncidenceGeometry.Point), IncidenceGeometry.OnLine k S ∧ IncidenceGeometry.OnLine k R ∧ IncidenceGeometry.B h b k ∧ ¬IncidenceGeometry.OnLine k Q

theorem SyntheticEuclid4.lines_inter_of_pgram' [I : IncidenceGeometry] {a b e f g h k : IncidenceGeometry.Point} {L M N P Q R S : IncidenceGeometry.Line} (Babe : IncidenceGeometry.B a b e) (Bfgh : IncidenceGeometry.B f g h) (pgram1 : paragram f g b e Q P L R) (pgram2 : paragram a b g h L P Q M) (bS : IncidenceGeometry.OnLine b S) (hS : IncidenceGeometry.OnLine h S) (kS : IncidenceGeometry.OnLine k S) (kR : IncidenceGeometry.OnLine k R) (kN : IncidenceGeometry.OnLine k N) (paraMR : para M R) (paraLN : para L N) (paraQN : para Q N) : ∃ (m : IncidenceGeometry.Point), IncidenceGeometry.OnLine m P ∧ IncidenceGeometry.OnLine m N ∧ IncidenceGeometry.B g b m

theorem SyntheticEuclid4.pgram_seg_of_tri_ang [I : IncidenceGeometry] {a b i j : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} {n o p q s : IncidenceGeometry.Point} (ab : a ≠ b) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (tri_nop : triangle n o p) (tri_qrs : triangle q j s) (iL : ¬IncidenceGeometry.OnLine i L) : ∃ (l : IncidenceGeometry.Point) (m : IncidenceGeometry.Point) (M : IncidenceGeometry.Line) (N : IncidenceGeometry.Line) (O : IncidenceGeometry.Line), paragram a b m l L M N O ∧ IncidenceGeometry.area l b a + IncidenceGeometry.area l b m = IncidenceGeometry.area n o p ∧ IncidenceGeometry.angle a b m = IncidenceGeometry.angle q j s ∧ diffside m i L

Euclid I.44, make a parallelogram on a segment with a prescribed area and angle

theorem SyntheticEuclid4.pgram_of_quad [I : IncidenceGeometry] {a b c d e f i j : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} {n p : IncidenceGeometry.Point} (nf : n ≠ f) (tri_abd : triangle a b d) (tri_cbd : triangle c b d) (tri_eij : triangle e i j) (nL : IncidenceGeometry.OnLine n L) (fL : IncidenceGeometry.OnLine f L) (pL : ¬IncidenceGeometry.OnLine p L) : ∃ (k : IncidenceGeometry.Point) (m : IncidenceGeometry.Point) (l : IncidenceGeometry.Point) (M : IncidenceGeometry.Line) (N : IncidenceGeometry.Line) (O : IncidenceGeometry.Line), IncidenceGeometry.B n f k ∧ paragram f k m l L M N O ∧ IncidenceGeometry.area f m k + IncidenceGeometry.area f m l = IncidenceGeometry.area a b d + IncidenceGeometry.area c b d ∧ IncidenceGeometry.angle k f l = IncidenceGeometry.angle e i j ∧ IncidenceGeometry.SameSide l p L

Euclid I.45, from a quadrilateral contructing a parallelogram with its area

theorem SyntheticEuclid4.square_of_len [I : IncidenceGeometry] {a b f : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (ab : a ≠ b) (aL : IncidenceGeometry.OnLine a L) (bL : IncidenceGeometry.OnLine b L) (fL : ¬IncidenceGeometry.OnLine f L) : ∃ (c : IncidenceGeometry.Point) (d : IncidenceGeometry.Point) (M : IncidenceGeometry.Line) (N : IncidenceGeometry.Line) (O : IncidenceGeometry.Line), paragram a b d c L O M N ∧ square a c d b ∧ diffside c f L

Euclid I.46, constructing a square out of a segment

theorem SyntheticEuclid4.ne_of_perp_ineq [I : IncidenceGeometry] {a b c d x y : IncidenceGeometry.Point} {L : IncidenceGeometry.Line} (Bxdy : IncidenceGeometry.B x d y) (tri_abc : triangle a b c) (bL : IncidenceGeometry.OnLine b L) (cL : IncidenceGeometry.OnLine c L) (xL : IncidenceGeometry.OnLine x L) (cab_le_ra : IncidenceGeometry.rightangle ≤ IncidenceGeometry.angle c a b) (ady : IncidenceGeometry.angle a d y = IncidenceGeometry.rightangle) : b ≠ d

theorem SyntheticEuclid4.not_B_of_right_le_right [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} (tri_abc : triangle a b c) (col_bcd : colinear b c d) (adb : IncidenceGeometry.angle a d b = IncidenceGeometry.rightangle) (cab_le_ra : IncidenceGeometry.rightangle ≤ IncidenceGeometry.angle c a b) : ¬IncidenceGeometry.B d b c

theorem SyntheticEuclid4.right_B_of_le_right [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri_abc : triangle a b c) (cab_le_ra : IncidenceGeometry.rightangle ≤ IncidenceGeometry.angle c a b) : ∃ (d : IncidenceGeometry.Point), IncidenceGeometry.angle a d b = IncidenceGeometry.rightangle ∧ IncidenceGeometry.angle a d c = IncidenceGeometry.rightangle ∧ IncidenceGeometry.B b d c

A big enough angle has its perpendicular on a triangle side

theorem SyntheticEuclid4.pythagoras_construct [I : IncidenceGeometry] {a b c : IncidenceGeometry.Point} (tri_abc : triangle a b c) : ∃ (d : IncidenceGeometry.Point) (e : IncidenceGeometry.Point) (f : IncidenceGeometry.Point) (g : IncidenceGeometry.Point) (h : IncidenceGeometry.Point) (k : IncidenceGeometry.Point) (L : IncidenceGeometry.Line) (M : IncidenceGeometry.Line) (N : IncidenceGeometry.Line) (O : IncidenceGeometry.Line) (P : IncidenceGeometry.Line) (Q : IncidenceGeometry.Line) (R : IncidenceGeometry.Line) (S : IncidenceGeometry.Line) (T : IncidenceGeometry.Line) (U : IncidenceGeometry.Line) (V : IncidenceGeometry.Line) (W : IncidenceGeometry.Line), square c d e b ∧ square a g f b ∧ square a h k c ∧ paragram b c d e L O P Q ∧ paragram g a b f T N R S ∧ paragram h a c k U M W V ∧ diffside a d L ∧ diffside b h M ∧ diffside c g N

Euclid I.47, the construction of the squares for the Pythagorean theorem

theorem SyntheticEuclid4.pythagoras [I : IncidenceGeometry] {a b c d e f g h k : IncidenceGeometry.Point} {L M N O P Q R S T U W V : IncidenceGeometry.Line} (tri_abc : triangle a b c) (ang : IncidenceGeometry.angle c a b = IncidenceGeometry.rightangle) (sq1 : square c d e b) (sq2 : square a g f b) (sq3 : square a h k c) (pgram1 : paragram b c d e L O P Q) (pgram2 : paragram g a b f T N R S) (pgram3 : paragram h a c k U M W V) (adL : diffside a d L) (bhM : diffside b h M) (cgN : diffside c g N) : IncidenceGeometry.area b c d + IncidenceGeometry.area b d e = IncidenceGeometry.area a b f + IncidenceGeometry.area a g f + IncidenceGeometry.area a h k + IncidenceGeometry.area a c k

Euclid I.47, the Pythagorean theorem

theorem SyntheticEuclid4.length_eq_of_square_eq [I : IncidenceGeometry] {a b c d : IncidenceGeometry.Point} {L M N O P Q R S : IncidenceGeometry.Line} {b' a' d' c' : IncidenceGeometry.Point} (sq1 : square a b b' a') (sq2 : square c d d' c') (pgram1 : paragram a b b' a' L M N O) (pgram2 : paragram c d d' c' P Q R S) (areas_eq : IncidenceGeometry.area a b a' + IncidenceGeometry.area a' b b' = IncidenceGeometry.area c d c' + IncidenceGeometry.area c' d d') : IncidenceGeometry.length a b = IncidenceGeometry.length c d

Lemma for I.48

theorem SyntheticEuclid4.pythagoras_converse [I : IncidenceGeometry] {a b c d e f g h k : IncidenceGeometry.Point} {L M N O P Q R S T U W V : IncidenceGeometry.Line} (tri_abc : triangle a b c) (sq1 : square c d e b) (sq2 : square a g f b) (sq3 : square a h k c) (pgram1 : paragram b c d e L O P Q) (pgram2 : paragram g a b f T N R S) (pgram3 : paragram h a c k U M W V) (_adL : diffside a d L) (_bhM : diffside b h M) (_cgN : diffside c g N) (sq_sum : IncidenceGeometry.area b c d + IncidenceGeometry.area b d e = IncidenceGeometry.area a b f + IncidenceGeometry.area a g f + IncidenceGeometry.area a h k + IncidenceGeometry.area a c k) : IncidenceGeometry.angle b a c = IncidenceGeometry.rightangle

Euclid I.48, the converse to the Pythagorean theorem