proposition: Theorem stronger_postulates_ter : stronger (existential_thales_postulate:: posidonius_postulate:: postulate_of_existence_of_a_right_lambert_quadrilateral:: postulate_of_existence_of_a_right_saccheri_quadrilateral:: postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights:: postulate_of_existence_of_similar_triangles:: postulate_of_right_lambert_quadrilaterals:: postulate_of_right_saccheri_quadrilaterals:: thales_postulate:: thales_converse_postulate:: triangle_postulate:: nil) (legendre_s_parallel_postulate:: bachmann_s_lotschnittaxiom:: weak_inverse_projection_postulate:: weak_tarski_s_parallel_postulate:: weak_triangle_circumscription_principle:: nil).
proof: Proof. assert(HPPWC1:=equivalent_postulates_without_any_continuity). assert(HPPWC2:=equivalent_postulates_without_any_continuity_bis). assert(H:=thales_converse_postulate__weak_triangle_circumscription_principle). assert(I:=bachmann_s_lotschnittaxiom__legendre_s_parallel_postulate). replace(legendre_s_parallel_postulate::bachmann_s_lotschnittaxiom::weak_inverse_projection_postulate:: weak_tarski_s_parallel_postulate::weak_triangle_circumscription_principle::nil) with ((legendre_s_parallel_postulate::nil) ++ bachmann_s_lotschnittaxiom::weak_inverse_projection_postulate::weak_tarski_s_parallel_postulate:: weak_triangle_circumscription_principle::nil); [|simpl; reflexivity]. assert(stronger(existential_thales_postulate::posidonius_postulate:: postulate_of_existence_of_a_right_lambert_quadrilateral:: postulate_of_existence_of_a_right_saccheri_quadrilateral:: postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights:: postulate_of_existence_of_similar_triangles::postulate_of_right_lambert_quadrilaterals:: postulate_of_right_saccheri_quadrilaterals::thales_postulate::thales_converse_postulate:: triangle_postulate::nil) (bachmann_s_lotschnittaxiom::weak_inverse_projection_postulate::weak_tarski_s_parallel_postulate:: weak_triangle_circumscription_principle::nil)) by (apply all_equiv2_impl__stronger with thales_converse_postulate weak_triangle_circumscription_principle; trivial; inlist). apply stronger2__stronger_right; trivial. eapply stronger_transitivity; eauto; [|discriminate]. apply all_equiv2_impl__stronger with bachmann_s_lotschnittaxiom legendre_s_parallel_postulate; simpl; auto. apply all_equiv_trivial. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.SPP_tarski GeoCoq.Meta_theory.Parallel_postulates.alternate_interior_angles_consecutive_interior_angles GeoCoq.Meta_theory.Parallel_postulates.alternate_interior_angles_playfair_bis GeoCoq.Meta_theory.Parallel_postulates.alternate_interior_angles_triangle GeoCoq.Meta_theory.Parallel_postulates.alternate_interior_angles_proclus GeoCoq.Meta_theory.Parallel_postulates.bachmann_s_lotschnittaxiom_legendre_s_parallel_postulate GeoCoq.Meta_theory.Parallel_postulates.bachmann_s_lotschnittaxiom_weak_inverse_projection_postulate GeoCoq.Meta_theory.Parallel_postulates.bachmann_s_lotschnittaxiom_weak_triangle_circumscription_principle GeoCoq.Meta_theory.Parallel_postulates.consecutive_interior_angles_alternate_interior_angles GeoCoq.Meta_theory.Parallel_postulates.existential_playfair_rah GeoCoq.Meta_theory.Parallel_postulates.existential_saccheri_rah GeoCoq.Meta_theory.Parallel_postulates.inverse_projection_postulate_proclus_bis GeoCoq.Meta_theory.Parallel_postulates.legendre GeoCoq.Meta_theory.Parallel_postulates.midpoint_playfair GeoCoq.Meta_theory.Parallel_postulates.original_euclid_original_spp GeoCoq.Meta_theory.Parallel_postulates.original_spp_inverse_projection_postulate GeoCoq.Meta_theory.Parallel_postulates.par_perp_2_par_par_perp_perp GeoCoq.Meta_theory.Parallel_postulates.par_perp_perp_par_perp_2_par GeoCoq.Meta_theory.Parallel_postulates.par_perp_perp_playfair GeoCoq.Meta_theory.Parallel_postulates.par_trans_playfair GeoCoq.Meta_theory.Parallel_postulates.playfair_existential_playfair GeoCoq.Meta_theory.Parallel_postulates.playfair_midpoint GeoCoq.Meta_theory.Parallel_postulates.playfair_par_trans GeoCoq.Meta_theory.Parallel_postulates.posidonius_postulate_rah GeoCoq.Meta_theory.Parallel_postulates.proclus_aristotle GeoCoq.Meta_theory.Parallel_postulates.proclus_bis_proclus GeoCoq.Meta_theory.Parallel_postulates.rah_existential_saccheri GeoCoq.Meta_theory.Parallel_postulates.rah_rectangle_principle GeoCoq.Meta_theory.Parallel_postulates.rah_similar GeoCoq.Meta_theory.Parallel_postulates.rah_thales_postulate GeoCoq.Meta_theory.Parallel_postulates.rah_posidonius_postulate GeoCoq.Meta_theory.Parallel_postulates.rectangle_existence_rah GeoCoq.Meta_theory.Parallel_postulates.rectangle_principle_rectangle_existence GeoCoq.Meta_theory.Parallel_postulates.similar_rah GeoCoq.Meta_theory.Parallel_postulates.tarski_playfair GeoCoq.Meta_theory.Parallel_postulates.thales_converse_postulate_thales_existence GeoCoq.Meta_theory.Parallel_postulates.thales_converse_postulate_weak_triangle_circumscription_principle GeoCoq.Meta_theory.Parallel_postulates.thales_existence_rah GeoCoq.Meta_theory.Parallel_postulates.thales_postulate_thales_converse_postulate GeoCoq.Meta_theory.Parallel_postulates.weak_inverse_projection_postulate_bachmann_s_lotschnittaxiom GeoCoq.Meta_theory.Parallel_postulates.weak_inverse_projection_postulate_weak_tarski_s_parallel_postulate GeoCoq.Meta_theory.Parallel_postulates.weak_tarski_s_parallel_postulate_weak_inverse_projection_postulate GeoCoq.Meta_theory.Parallel_postulates.weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom GeoCoq.Tarski_dev.Annexes.saccheri GeoCoq.Tarski_dev.Annexes.perp_bisect GeoCoq.Tarski_dev.Annexes.quadrilaterals GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Utils.all_equiv Rtauto