proposition: Theorem equivalent_postulates_assuming_greenberg_s_axiom : greenberg_s_axiom -> all_equiv (alternate_interior_angles_postulate:: alternative_playfair_s_postulate:: alternative_proclus_postulate:: alternative_strong_parallel_postulate:: consecutive_interior_angles_postulate:: euclid_5:: euclid_s_parallel_postulate:: existential_playfair_s_postulate:: existential_thales_postulate:: inverse_projection_postulate:: midpoint_converse_postulate:: perpendicular_transversal_postulate:: postulate_of_transitivity_of_parallelism:: playfair_s_postulate:: posidonius_postulate:: universal_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_parallelism_of_perpendicular_transversals:: postulate_of_right_lambert_quadrilaterals:: postulate_of_right_saccheri_quadrilaterals:: postulate_of_transitivity_of_parallelism:: proclus_postulate:: strong_parallel_postulate:: tarski_s_parallel_postulate:: thales_postulate:: thales_converse_postulate:: triangle_circumscription_principle:: triangle_postulate:: nil).
proof: Proof. intro HG. assert (He : all_equiv ( (existential_playfair_s_postulate::nil) ++ ((alternate_interior_angles_postulate::alternative_playfair_s_postulate:: alternative_proclus_postulate::alternative_strong_parallel_postulate:: consecutive_interior_angles_postulate::euclid_5::euclid_s_parallel_postulate:: inverse_projection_postulate::midpoint_converse_postulate::perpendicular_transversal_postulate:: playfair_s_postulate::universal_posidonius_postulate:: postulate_of_parallelism_of_perpendicular_transversals::postulate_of_transitivity_of_parallelism:: proclus_postulate::strong_parallel_postulate::tarski_s_parallel_postulate:: triangle_circumscription_principle::nil) ++ (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)))). { assert (He : all_equiv ( (alternate_interior_angles_postulate::alternative_playfair_s_postulate:: alternative_proclus_postulate::alternative_strong_parallel_postulate:: consecutive_interior_angles_postulate::euclid_5::euclid_s_parallel_postulate:: inverse_projection_postulate::midpoint_converse_postulate::perpendicular_transversal_postulate:: playfair_s_postulate::universal_posidonius_postulate:: postulate_of_parallelism_of_perpendicular_transversals::postulate_of_transitivity_of_parallelism:: proclus_postulate::strong_parallel_postulate::tarski_s_parallel_postulate:: triangle_circumscription_principle::nil) ++ (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))). { assert (HPP : all_equiv (alternate_interior_angles_postulate::alternative_playfair_s_postulate:: alternative_proclus_postulate::alternative_strong_parallel_postulate:: consecutive_interior_angles_postulate::euclid_5::euclid_s_parallel_postulate:: inverse_projection_postulate::midpoint_converse_postulate::perpendicular_transversal_postulate:: playfair_s_postulate::universal_posidonius_postulate:: postulate_of_parallelism_of_perpendicular_transversals::postulate_of_transitivity_of_parallelism:: proclus_postulate::strong_parallel_postulate::tarski_s_parallel_postulate:: triangle_circumscription_principle::nil)). { rewrite all_equiv_chara; intros x y HxIn HyIn Hx. assert (HID : decidability_of_intersection). { assert(HADG:=equivalence_of_aristotle_greenberg_and_decidability_of_intersection). rewrite <- (HADG x greenberg_s_axiom); simpl; auto. } assert(HPP:=equivalent_postulates_with_decidability_of_intersection_of_lines). rewrite <- (HPP HID x); trivial. } assert (HPPWC := equivalent_postulates_without_any_continuity). apply all_equiv2_stronger2__all_equiv; trivial. { assert (HS : stronger ((alternative_strong_parallel_postulate::alternative_proclus_postulate:: euclid_5::euclid_s_parallel_postulate::inverse_projection_postulate::proclus_postulate:: strong_parallel_postulate::tarski_s_parallel_postulate::triangle_circumscription_principle:: nil) ++ (alternate_interior_angles_postulate:: alternative_playfair_s_postulate:: consecutive_interior_angles_postulate::midpoint_converse_postulate:: perpendicular_transversal_postulate::playfair_s_postulate::universal_posidonius_postulate:: postulate_of_parallelism_of_perpendicular_transversals:: postulate_of_transitivity_of_parallelism::nil)) (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)). { assert (HSB := stronger_postulates_bis). apply stronger2__stronger_left; [|assumption]. assert (HS := stronger_postulates). eapply stronger_transitivity; eauto; discriminate. } eapply incl_preserves_stronger; eauto; [|apply incl_refl]. clear HG HPP HPPWC HS; intros a H; repeat induction H; inlist. } { assert (I:=triangle__playfair_bis HG). apply all_equiv2_impl__stronger with triangle_postulate alternative_playfair_s_postulate; trivial; inlist. } } assert(H:=existential_playfair__rah). assert(I:=playfair__existential_playfair). assert(J:=all_equiv_trivial existential_playfair_s_postulate). apply all_equiv2_impl2__all_equiv with existential_playfair_s_postulate postulate_of_right_saccheri_quadrilaterals playfair_s_postulate existential_playfair_s_postulate; trivial; inlist. } eapply incl_preserves_all_equiv; eauto. clear HG He; intros a H; repeat induction H; inlist. 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