proposition: Lemma legendre_aux : ~ hypothesis_of_obtuse_saccheri_quadrilaterals -> forall A B C D B1 C1 P Q R S T U V W X, ~ Col A B C -> CongA A C B C B D -> Cong A C B D -> TS B C A D -> Out A B B1 -> Out A C C1 -> Bet B1 D C1 -> Defect A B C P Q R -> Defect A B1 C1 S T U -> SumA P Q R P Q R V W X -> SAMS P Q R P Q R /\ LeA V W X S T U.
proof: Proof. intros noah A B C D B1 C1 P Q R S T U V W X HNCol HConga HCong HTS HOutB HOutC HBet HDef HDef1 HSuma. destruct (l11_49 A C B D B C) as [HCong1 [HConga1 HConga2]]; CongA; Cong. assert_diffs; auto. assert (HPar : Par_strict A C B D). { apply par_not_col_strict with B; Col. apply par_left_comm, l12_21_b; Side; CongA. } assert (HPar' : Par_strict A B C D). { apply par_not_col_strict with C; Col. apply par_left_comm, l12_21_b; Side; CongA. } assert (HNCol2:= HPar'); assert (HNCol3 := HPar'); assert (HNCol4 := HPar'). apply par_strict_not_col_2 in HNCol2; apply par_strict_not_col_3 in HNCol3; apply par_strict_not_col_4 in HNCol4. assert (HB : ~ Col B1 B D /\ TS B D B1 C1 /\ Bet A B B1). { assert_diffs. apply par_strict_symmetry, (par_strict_col_par_strict B D A C C1) in HPar; Col. assert (HNCol' := par_strict_not_col_4 B D A C1 HPar). assert (B <> B1) by (intro; subst B1; apply HNCol'; Col). assert (~ Col B1 B D) by (intro; apply HNCol4; ColR). assert (TS B D B1 C1) by (repeat split; Col; exists D; Col). repeat (split; auto). apply col_two_sides_bet with D; Col. apply l9_8_2 with C1; Side. } destruct HB as [HNCol5 [HTS1 HBetB]]. assert (HC : ~ Col C D B1 /\ C <> C1 /\ Bet A C C1). { assert_diffs. apply par_strict_symmetry, (par_strict_col_par_strict C D A B B1) in HPar'; Col. assert (HNCol' := par_strict_not_col_4 C D A B1 HPar'). assert (C <> C1) by (intro; subst C1; apply HNCol'; Col). repeat split; auto. apply col_two_sides_bet with D; Col. apply l9_8_2 with B1; Side. repeat split; Col. intro; apply HNCol3; ColR. exists D; Col. } destruct HC as [HNCol6 [HCC1 HBetC]]. assert_diffs. destruct (ts2__ex_bet2 B C D B1) as [Z [HZ1 HZ2]]. apply l9_8_2 with C1; Side; apply one_side_symmetry, l12_6, par_strict_col_par_strict with A; Col; Par. { apply l9_31. apply l9_17 with C1; trivial. exists A; repeat split; Col; try (intro; apply HNCol; ColR); [exists B|exists C]; split; Col; Between. apply one_side_symmetry, l12_6, par_strict_col_par_strict with A; Col; Par. } rename H into HAB1. destruct (ex_defect A B1 C) as [G [H [I HDef2]]]; auto. destruct (ex_defect B1 C C1) as [J [K [L HDef3]]]; auto. destruct (ex_defect C B B1) as [M [N [O HDef4]]]; auto. destruct (ex_defect B1 C D) as [A' [B' [C' HDef5]]]; auto. destruct (ex_defect C D C1) as [D' [E' [F' HDef6]]]; auto. destruct (ex_defect B1 B D) as [M' [N' [O' HDef7]]]; auto. assert (Hd := defect_distincts A B1 C G H I HDef2). assert (Hd2 := defect_distincts C B B1 M N O HDef4). assert (Hd3 := defect_distincts B1 C D A' B' C' HDef5). spliter; clean. destruct (ex_suma G H I A' B' C') as [G' [H' [I' HSuma1]]]; auto. destruct (ex_suma M N O A' B' C') as [J' [K' [L' HSuma2]]]; auto. destruct (t22_16_1bis noah A B1 C1 C G H I J K L S T U) as [HIsi3 HSuma3]; trivial. destruct (t22_16_1bis noah B1 C C1 D A' B' C' D' E' F' J K L) as [HIsi4 HSuma4]; trivial. destruct (t22_16_1bis noah A C B1 B P Q R M N O G H I) as [HIsi5 HSuma5]; trivial. apply defect_perm_132, HDef. apply defect_perm_132, HDef2. assert (HIsi1 : SAMS G H I A' B' C'). apply sams_lea2__sams with G H I J K L; Lea. apply sams_suma__lea123789 with D' E' F'; trivial. assert (HIsi2 : SAMS M N O A' B' C'). apply sams_lea2__sams with G H I A' B' C'; Lea. apply sams_suma__lea456789 with P Q R; trivial. assert (HSuma6 : SumA G' H' I' D' E' F' S T U). apply suma_assoc_2 with G H I A' B' C' J K L; trivial. assert (HIsi6 : SAMS G' H' I' D' E' F'). apply sams_assoc_2 with G H I A' B' C' J K L; trivial. assert (HSuma7 : SumA P Q R J' K' L' G' H' I'). apply suma_assoc_1 with M N O A' B' C' G H I; trivial. assert (HIsi7 : SAMS P Q R J' K' L'). apply sams_assoc_1 with M N O A' B' C' G H I; trivial. destruct (t22_16_2 noah C B B1 D M' N' O' A' B' C' P Q R M N O Z J' K' L') as [HIsi8 HSuma8]; trivial. apply defect_perm_231, (conga3_defect__defect A B C); CongA. apply defect_perm_231, HDef5. assert (HLea : LeA P Q R J' K' L') by (apply sams_suma__lea123789 with M' N' O'; trivial). split. suma.assert_diffs. apply sams_lea2__sams with P Q R J' K' L'; Lea. apply lea_trans with G' H' I'. apply sams_lea456_suma2__lea with P Q R P Q R J' K' L'; trivial. apply sams_suma__lea123789 with D' E' F'; trivial. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.SPP_ID GeoCoq.Meta_theory.Parallel_postulates.TCP_tarski GeoCoq.Meta_theory.Parallel_postulates.alternate_interior_angles_proclus GeoCoq.Meta_theory.Continuity.angle_archimedes GeoCoq.Meta_theory.Continuity.archimedes GeoCoq.Meta_theory.Continuity.aristotle GeoCoq.Meta_theory.Parallel_postulates.euclid_5_original_euclid GeoCoq.Meta_theory.Parallel_postulates.existential_triangle_rah GeoCoq.Meta_theory.Parallel_postulates.par_perp_perp_TCP GeoCoq.Meta_theory.Parallel_postulates.playfair_alternate_interior_angles GeoCoq.Meta_theory.Parallel_postulates.playfair_bis_playfair GeoCoq.Meta_theory.Parallel_postulates.playfair_universal_posidonius_postulate GeoCoq.Meta_theory.Parallel_postulates.proclus_SPP GeoCoq.Meta_theory.Parallel_postulates.rah_triangle GeoCoq.Meta_theory.Parallel_postulates.tarski_euclid GeoCoq.Meta_theory.Parallel_postulates.triangle_playfair_bis GeoCoq.Meta_theory.Parallel_postulates.triangle_existential_triangle GeoCoq.Meta_theory.Parallel_postulates.universal_posidonius_postulate_par_perp_perp GeoCoq.Tarski_dev.Annexes.defect