proposition: Lemma legendre_s_fourth_theorem_aux : archimedes_axiom -> legendre_s_parallel_postulate -> postulate_of_right_saccheri_quadrilaterals.
proof: Proof. intros archi legendre. destruct legendre as [B [A [C [HNCol [HAcute legendre]]]]]. assert_diffs. destruct (ex_defect A B C) as [P [Q [R HDef]]]; auto. destruct (col_dec P Q R) as [HCol|HNCol1]. - apply archi__obtuse_case_elimination in archi. apply (defect_ncol_out__rah A B C P Q R); Col. apply not_bet_out; Col. intro HBet. apply HNCol. apply defect_perm_213 in HDef. destruct HDef as [D [E [F [[G [H [I [HSuma1 HSuma2]]]] HSuppa]]]]. apply out_col, l6_6, out_lea__out with D E F. apply (bet_suppa__out P Q R); [|apply suppa_sym]; assumption. apply sams_suma__lea456789 with G H I; trivial. apply (t22_20 archi); trivial. - destruct (archi__gradaexp_destruction archi P Q R HNCol1) as [S [T [U [HGAE HObtuse]]]]. apply archi__obtuse_case_elimination in archi. apply not_col_permutation_4 in HNCol. destruct (legendre_aux2 archi A B C HNCol HAcute legendre P Q R S T U HDef HGAE) as [B' [C' HInter]]. destruct HInter as [P' [Q' [R' [HOutB [HOutC [HDef' HLea]]]]]]. apply (lea_obtuse_obtuse P' Q' R'), obtuse__nsams in HObtuse; auto. exfalso. apply HObtuse. destruct (legendre_aux1 A B C B' C') as [D' [HInangle [HConga [HCong HTS]]]]; trivial. assert (HNCol' : ~ Col A B' C') by (destruct HTS; Col). destruct (legendre D' HInangle) as [B'' [C'' [HOutB' [HOutC' HBet]]]]. assert_diffs. destruct (ex_defect A B'' C'') as [S' [T' [U' HDef'']]]; auto. intro; subst; apply HNCol; ColR. destruct (ex_suma P' Q' R' P' Q' R') as [V [W [X HSuma]]]; auto. destruct (legendre_aux archi A B' C' D' B'' C'' P' Q' R' S' T' U' V W X); trivial; [apply l6_7 with B|apply l6_7 with C]; Out. 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