proposition: Theorem equivalence_of_aristotle_greenberg_and_decidability_of_intersection : all_equiv_under (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) (aristotle_s_axiom:: greenberg_s_axiom:: decidability_of_intersection:: nil).
proof: Proof. apply all_equiv_under_chara. intros x HInx Hx. cut playfair_s_postulate; [intro HP; clear dependent x|]. { apply all_equiv__equiv; unfold all_equiv; simpl. split. { intro I; apply proclus__aristotle. revert HP. apply (equivalent_postulates_with_decidability_of_intersection_of_lines I); inlist. } split; [apply aristotle__greenberg|repeat split]. { intros HG. cut proclus_postulate. { intro HP'. apply strong_parallel_postulate_implies_inter_dec. revert HP'. apply equivalent_postulates_without_decidability_of_intersection_of_lines_bis; inlist. } apply (alternate_interior__proclus HG). revert HP. apply equivalent_postulates_without_decidability_of_intersection_of_lines; inlist. } } { assert (H:=stronger_postulates). assert (I:=equivalent_postulates_without_decidability_of_intersection_of_lines). unfold stronger, all_equiv in *; simpl in H; simpl in I; simpl in HInx; decompose [or] HInx; clear HInx; subst; try rtauto; let A := type of Hx in (try (apply (H A); try tauto; rtauto); try (apply -> (I A); try tauto; rtauto)). } 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