proposition: Lemma legendre_s_third_theorem_aux : aristotle_s_axiom -> triangle_postulate -> euclid_s_parallel_postulate.
proof: Proof. intros HA HT. apply aristotle__greenberg in HA. apply triangle__playfair_bis in HT; trivial. apply playfair_bis__playfair in HT. apply euclid_5__original_euclid, tarski_s_euclid_implies_euclid_5. apply triangle_circumscription_implies_tarski_s_euclid. apply inter_dec_plus_par_perp_perp_imply_triangle_circumscription. { apply strong_parallel_postulate_implies_inter_dec. apply proclus_s_postulate_implies_strong_parallel_postulate. apply alternate_interior__proclus; trivial. apply playfair__alternate_interior, HT. } apply universal_posidonius_postulate__perpendicular_transversal_postulate. apply playfair__universal_posidonius_postulate, HT. 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