Require Import GeoCoq.Axioms.continuity_axioms.
Require Export GeoCoq.Axioms.parallel_postulates.
Require Export GeoCoq.Meta_theory.Parallel_postulates.SPP_tarski.
Require Export GeoCoq.Meta_theory.Parallel_postulates.alternate_interior_angles_consecutive_interior_angles.
Require Export GeoCoq.Meta_theory.Parallel_postulates.alternate_interior_angles_playfair_bis.
Require Export GeoCoq.Meta_theory.Parallel_postulates.alternate_interior_angles_triangle.
Require Export GeoCoq.Meta_theory.Parallel_postulates.alternate_interior_angles_proclus.
Require Export GeoCoq.Meta_theory.Parallel_postulates.bachmann_s_lotschnittaxiom_legendre_s_parallel_postulate.
Require Export GeoCoq.Meta_theory.Parallel_postulates.bachmann_s_lotschnittaxiom_weak_inverse_projection_postulate.
Require Export GeoCoq.Meta_theory.Parallel_postulates.bachmann_s_lotschnittaxiom_weak_triangle_circumscription_principle.
Require Export GeoCoq.Meta_theory.Parallel_postulates.consecutive_interior_angles_alternate_interior_angles.
Require Export GeoCoq.Meta_theory.Parallel_postulates.existential_playfair_rah.
Require Export GeoCoq.Meta_theory.Parallel_postulates.existential_saccheri_rah.
Require Export GeoCoq.Meta_theory.Parallel_postulates.inverse_projection_postulate_proclus_bis.
Require Export GeoCoq.Meta_theory.Parallel_postulates.legendre.
Require Export GeoCoq.Meta_theory.Parallel_postulates.midpoint_playfair.
Require Export GeoCoq.Meta_theory.Parallel_postulates.original_euclid_original_spp.
Require Export GeoCoq.Meta_theory.Parallel_postulates.original_spp_inverse_projection_postulate.
Require Export GeoCoq.Meta_theory.Parallel_postulates.par_perp_2_par_par_perp_perp.
Require Export GeoCoq.Meta_theory.Parallel_postulates.par_perp_perp_par_perp_2_par.
Require Export GeoCoq.Meta_theory.Parallel_postulates.par_perp_perp_playfair.
Require Export GeoCoq.Meta_theory.Parallel_postulates.par_trans_playfair.
Require Export GeoCoq.Meta_theory.Parallel_postulates.playfair_existential_playfair.
Require Export GeoCoq.Meta_theory.Parallel_postulates.playfair_midpoint.
Require Export GeoCoq.Meta_theory.Parallel_postulates.playfair_par_trans.
Require Export GeoCoq.Meta_theory.Parallel_postulates.posidonius_postulate_rah.
Require Export GeoCoq.Meta_theory.Parallel_postulates.proclus_aristotle.
Require Export GeoCoq.Meta_theory.Parallel_postulates.proclus_bis_proclus.
Require Export GeoCoq.Meta_theory.Parallel_postulates.rah_existential_saccheri.
Require Export GeoCoq.Meta_theory.Parallel_postulates.rah_rectangle_principle.
Require Export GeoCoq.Meta_theory.Parallel_postulates.rah_similar.
Require Export GeoCoq.Meta_theory.Parallel_postulates.rah_thales_postulate.
Require Export GeoCoq.Meta_theory.Parallel_postulates.rah_posidonius_postulate.
Require Export GeoCoq.Meta_theory.Parallel_postulates.rectangle_existence_rah.
Require Export GeoCoq.Meta_theory.Parallel_postulates.rectangle_principle_rectangle_existence.
Require Export GeoCoq.Meta_theory.Parallel_postulates.similar_rah.
Require Export GeoCoq.Meta_theory.Parallel_postulates.tarski_playfair.
Require Export GeoCoq.Meta_theory.Parallel_postulates.thales_converse_postulate_thales_existence.
Require Export GeoCoq.Meta_theory.Parallel_postulates.thales_converse_postulate_weak_triangle_circumscription_principle.
Require Export GeoCoq.Meta_theory.Parallel_postulates.thales_existence_rah.
Require Export GeoCoq.Meta_theory.Parallel_postulates.thales_postulate_thales_converse_postulate.
Require Export GeoCoq.Meta_theory.Parallel_postulates.weak_inverse_projection_postulate_bachmann_s_lotschnittaxiom.
Require Export GeoCoq.Meta_theory.Parallel_postulates.weak_inverse_projection_postulate_weak_tarski_s_parallel_postulate.
Require Export GeoCoq.Meta_theory.Parallel_postulates.weak_tarski_s_parallel_postulate_weak_inverse_projection_postulate.
Require Export GeoCoq.Meta_theory.Parallel_postulates.weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom.
Require Export GeoCoq.Tarski_dev.Annexes.saccheri.
Require Export GeoCoq.Tarski_dev.Annexes.perp_bisect.
Require Export GeoCoq.Tarski_dev.Annexes.quadrilaterals.
Require Export GeoCoq.Tarski_dev.Ch13_1.

Require Import GeoCoq.Utils.all_equiv.

Require Import Rtauto.

Section Euclid.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Theorem equivalent_postulates_without_decidability_of_intersection_of_lines :
  all_equiv
    (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).
Proof.
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) *)
assert (K:=alternate_interior__consecutive_interior).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) *)
assert (L:=alternate_interior__playfair_bis).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) *)
assert (M:=consecutive_interior__alternate_interior).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) *)
assert (N:=midpoint_converse_postulate_implies_playfair).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) *)
assert (O:=par_perp_perp_implies_par_perp_2_par).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) *)
assert (P:=par_perp_perp_implies_playfair).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) *)
assert (Q:=par_perp_2_par_implies_par_perp_perp).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) *)
assert (R:=par_trans_implies_playfair).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) *)
assert (S:=playfair_bis__playfair).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) *)
assert (T:=playfair_implies_par_trans).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) *)
assert (U:=playfair_s_postulate_implies_midpoint_converse_postulate).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) *)
assert (V:=playfair__alternate_interior).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) *)
assert (W:=playfair__universal_posidonius_postulate).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) *)
assert (X:=universal_posidonius_postulate__perpendicular_transversal_postulate).
(* Goal: all_equiv (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
apply all_equiv__equiv; unfold all_equiv'; simpl; repeat (split; tauto).
Qed.

Theorem equivalent_postulates_without_any_continuity :
  all_equiv
    (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).
Proof.
(* Goal: all_equiv (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
intros.
(* Goal: all_equiv (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
assert (H:=existential_saccheri__rah).
(* Goal: all_equiv (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
assert (I:=existential_triangle__rah).
(* Goal: all_equiv (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
assert (J:=posidonius_postulate__rah).
(* Goal: all_equiv (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
assert (K:=rah__existential_saccheri).
(* Goal: all_equiv (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
assert (L:=rah__rectangle_principle).
(* Goal: all_equiv (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
assert (M:=rah__similar).
(* Goal: all_equiv (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
assert (N:=rah__thales_postulate).
(* Goal: all_equiv (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
assert (O:=rah__triangle).
(* Goal: all_equiv (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
assert (P:=rah__posidonius).
(* Goal: all_equiv (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
assert (Q:=rectangle_existence__rah).
(* Goal: all_equiv (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
assert (R:=rectangle_principle__rectangle_existence).
(* Goal: all_equiv (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
assert (S:=similar__rah).
(* Goal: all_equiv (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
assert (T:=thales_converse_postulate__thales_existence).
(* Goal: all_equiv (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
assert (U:=thales_existence__rah).
(* Goal: all_equiv (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
assert (V:=thales_postulate__thales_converse_postulate).
(* Goal: all_equiv (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
assert (W:=triangle__existential_triangle).
(* Goal: all_equiv (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
apply all_equiv__equiv; unfold all_equiv'; simpl; repeat (split; tauto).
Qed.

Theorem equivalent_postulates_with_decidability_of_intersection_of_lines :
  decidability_of_intersection ->
  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).
Proof.
(* Goal: forall _ : @decidability_of_intersection Tn, all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) *)
intro HID.
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) *)
assert (L:=euclid_5__original_euclid).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) *)
assert (M:=inter_dec_plus_par_perp_perp_imply_triangle_circumscription HID); clear HID.
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) *)
assert (O:=inverse_projection_postulate__proclus_bis).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) *)
assert (P:=original_euclid__original_spp).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) *)
assert (Q:=original_spp__inverse_projection_postulate).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) *)
assert (R:=proclus_bis__proclus).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) *)
assert (S:=proclus_s_postulate_implies_strong_parallel_postulate).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) *)
assert (T:=strong_parallel_postulate_implies_tarski_s_euclid).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) *)
assert (U:=tarski_s_euclid_implies_euclid_5).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) *)
assert (V:=tarski_s_euclid_implies_playfair).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) *)
assert (W:=triangle_circumscription_implies_tarski_s_euclid).
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) *)
assert (X:=equivalent_postulates_without_decidability_of_intersection_of_lines).
(* Goal: all_equiv (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) *)
apply all_equiv__equiv; unfold all_equiv, all_equiv' in *; simpl in *.
repeat (split; try rtauto; try (intro Z;
        assert (HP:playfair_s_postulate)
          by (try rtauto; let A := type of Z in (apply -> (X A); try assumption; tauto));
        assert (J:perpendicular_transversal_postulate)
          by (let A := type of HP in (apply -> (X A); try assumption; tauto));
        try rtauto; let A := type of HP in (apply -> (X A); try assumption; tauto))).
Qed.

(** Every postulate which states the existence of a point is equivalent *)
Theorem equivalent_postulates_without_decidability_of_intersection_of_lines_bis :
  all_equiv
    (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).
Proof.
(* Goal: all_equiv (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) *)
assert (K:=euclid_5__original_euclid).
(* Goal: all_equiv (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) *)
assert (L:=inverse_projection_postulate__proclus_bis).
(* Goal: all_equiv (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) *)
assert (M:=original_euclid__original_spp).
(* Goal: all_equiv (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) *)
assert (N:=original_spp__inverse_projection_postulate).
(* Goal: all_equiv (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) *)
assert (O:=proclus_bis__proclus).
(* Goal: all_equiv (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) *)
assert (P:=proclus_s_postulate_implies_strong_parallel_postulate).
(* Goal: all_equiv (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) *)
assert (Q:=strong_parallel_postulate_implies_inter_dec).
(* Goal: all_equiv (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) *)
assert (R:=strong_parallel_postulate_implies_tarski_s_euclid).
(* Goal: all_equiv (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) *)
assert (S:=tarski_s_euclid_implies_euclid_5).
(* Goal: all_equiv (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) *)
assert (T:=triangle_circumscription_implies_tarski_s_euclid).
(* Goal: y *)
assert (HPP:=equivalent_postulates_with_decidability_of_intersection_of_lines).
(* Goal: all_equiv (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) *)
apply all_equiv__equiv; unfold all_equiv, all_equiv' in *; simpl in *.
repeat (split; try (try rtauto; intro W;
                    assert (HID:decidability_of_intersection) by rtauto;
                    let HTW := type of W in (apply -> (HPP HID HTW); try tauto; rtauto))).
Qed.

Theorem stronger_postulates :
  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).
Proof.
(* Goal: stronger (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) *)
assert(H:=equivalent_postulates_without_decidability_of_intersection_of_lines_bis).
(* Goal: @playfair_s_postulate Tn *)
assert(I:=equivalent_postulates_without_decidability_of_intersection_of_lines).
(* Goal: stronger (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) *)
assert(J:=tarski_s_euclid_implies_playfair).
(* Goal: stronger (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) *)
apply all_equiv2_impl__stronger with tarski_s_parallel_postulate playfair_s_postulate; trivial; inlist.
Qed.

Theorem stronger_postulates_bis :
  stronger
    (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).
Proof.
(* Goal: stronger (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
assert(H:=equivalent_postulates_without_decidability_of_intersection_of_lines).
(* Goal: stronger (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
assert(I:=equivalent_postulates_without_any_continuity).
(* Goal: stronger (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop)))))))))) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
assert(J:=alternate_interior__triangle).
apply all_equiv2_impl__stronger with alternate_interior_angles_postulate triangle_postulate; trivial;
  inlist.
Qed.

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.
(* Goal: all_equiv_under (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) (@cons Prop (@aristotle_s_axiom Tn) (@cons Prop (@greenberg_s_axiom Tn) (@cons Prop (@decidability_of_intersection Tn) (@nil Prop)))) *)
apply all_equiv_under_chara.
(* Goal: forall (x : Prop) (_ : @List.In Prop x (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))))))))))))) (_ : x), all_equiv (@cons Prop (@aristotle_s_axiom Tn) (@cons Prop (@greenberg_s_axiom Tn) (@cons Prop (@decidability_of_intersection Tn) (@nil Prop)))) *)
intros x HInx Hx.
cut playfair_s_postulate;
[intro HP; clear dependent x|].
(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))))))))))))))))))))) *)
  {
(* Goal: all_equiv (@cons Prop (@aristotle_s_axiom Tn) (@cons Prop (@greenberg_s_axiom Tn) (@cons Prop (@decidability_of_intersection Tn) (@nil Prop)))) *)
  apply all_equiv__equiv; unfold all_equiv; simpl.
(* Goal: and (forall _ : @decidability_of_intersection Tn, @aristotle_s_axiom Tn) (and (forall _ : @aristotle_s_axiom Tn, @greenberg_s_axiom Tn) (and (forall _ : @greenberg_s_axiom Tn, @decidability_of_intersection Tn) True)) *)
  split.
(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))))))))))))))))))))) *)
    {
(* Goal: forall _ : @decidability_of_intersection Tn, @aristotle_s_axiom Tn *)
    intro I; apply proclus__aristotle.
(* Goal: @alternate_interior_angles_postulate Tn *)
    revert HP.
(* Goal: forall _ : @playfair_s_postulate Tn, @proclus_postulate Tn *)
    apply (equivalent_postulates_with_decidability_of_intersection_of_lines I); inlist.
    }
(* Goal: and (forall _ : @aristotle_s_axiom Tn, @greenberg_s_axiom Tn) (and (forall _ : @greenberg_s_axiom Tn, @decidability_of_intersection Tn) True) *)
  split; [apply aristotle__greenberg|repeat split].
(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))))))))))))))))))))) *)
    {
(* Goal: forall _ : @greenberg_s_axiom Tn, @decidability_of_intersection Tn *)
    intros HG.
(* Goal: @decidability_of_intersection Tn *)
    cut proclus_postulate.
(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))))))))))))))))))))) *)
      {
(* Goal: forall _ : @proclus_postulate Tn, @decidability_of_intersection Tn *)
      intro HP'.
(* Goal: forall A B C D : @Tpoint Tn, or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I A B) (@Col Tn I C D))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I A B) (@Col Tn I C D)))) *)
      apply strong_parallel_postulate_implies_inter_dec.
(* Goal: @strong_parallel_postulate Tn *)
      revert HP'.
(* Goal: forall _ : @proclus_postulate Tn, @strong_parallel_postulate Tn *)
      apply equivalent_postulates_without_decidability_of_intersection_of_lines_bis; inlist.
      }
(* Goal: @proclus_postulate Tn *)
    apply (alternate_interior__proclus HG).
(* Goal: @alternate_interior_angles_postulate Tn *)
    revert HP.
(* Goal: forall _ : @playfair_s_postulate Tn, @alternate_interior_angles_postulate Tn *)
    apply equivalent_postulates_without_decidability_of_intersection_of_lines; inlist.
    }
  }

(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))))))))))))))))))))) *)
  {
(* Goal: @playfair_s_postulate Tn *)
  assert (H:=stronger_postulates).
(* Goal: @playfair_s_postulate Tn *)
  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.

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.
(* Goal: forall _ : @greenberg_s_axiom Tn, all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) *)
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)))).

(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))))))))))))))))))))) *)
  {
  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))).

(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))))))))))))))))))))) *)
    {
    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)).

(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))))))))))))))))))))) *)
      {
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) *)
      rewrite all_equiv_chara; intros x y HxIn HyIn Hx.
(* Goal: y *)
      assert (HID : decidability_of_intersection).
(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))))))))))))))))))))) *)
        {
(* Goal: @decidability_of_intersection Tn *)
        assert(HADG:=equivalence_of_aristotle_greenberg_and_decidability_of_intersection).
(* Goal: @decidability_of_intersection Tn *)
        rewrite <- (HADG x greenberg_s_axiom); simpl; auto.
        }
(* Goal: y *)
      assert(HPP:=equivalent_postulates_with_decidability_of_intersection_of_lines).
(* Goal: y *)
      rewrite <- (HPP HID x); trivial.
      }

(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop))))))))))))) *)
    assert (HPPWC := equivalent_postulates_without_any_continuity).
(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop))))))))))))) *)
    apply all_equiv2_stronger2__all_equiv; trivial.

(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))))))))))))))))))))) *)
      {
      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)).
(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))))))))))))))))))))) *)
          {
(* Goal: stronger (@app Prop (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop))))))))))) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
          assert (HSB := stronger_postulates_bis).
(* Goal: stronger (@app Prop (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop))))))))))) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
          apply stronger2__stronger_left; [|assumption].
(* Goal: stronger (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
          assert (HS := stronger_postulates).
(* Goal: stronger (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
          eapply stronger_transitivity; eauto; discriminate.
          }
(* Goal: stronger (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) *)
        eapply incl_preserves_stronger; eauto; [|apply incl_refl].
(* Goal: @incl Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) (@app Prop (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop)))))))))) (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@nil Prop))))))))))) *)
        clear HG HPP HPPWC HS; intros a H; repeat induction H; inlist.
      }

(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))))))))))))))))))))) *)
      {
(* Goal: stronger (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) *)
      assert (I:=triangle__playfair_bis HG).
      apply all_equiv2_impl__stronger with triangle_postulate alternative_playfair_s_postulate; trivial;
        inlist.
      }

    }
(* Goal: all_equiv (@app Prop (@cons Prop (@existential_playfair_s_postulate Tn) (@nil Prop)) (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))) *)
  assert(H:=existential_playfair__rah).
(* Goal: all_equiv (@app Prop (@cons Prop (@existential_playfair_s_postulate Tn) (@nil Prop)) (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))) *)
  assert(I:=playfair__existential_playfair).
(* Goal: all_equiv (@app Prop (@cons Prop (@existential_playfair_s_postulate Tn) (@nil Prop)) (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))) *)
  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.

  }

(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))))))))))))))))))))) *)
eapply incl_preserves_all_equiv; eauto.
(* Goal: @incl Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@existential_playfair_s_postulate Tn) (@nil Prop)) (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))) *)
clear HG He; intros a H; repeat induction H; inlist.
Qed.

Theorem equivalent_postulates_without_any_continuity_bis :
  all_equiv
    (bachmann_s_lotschnittaxiom::
     weak_inverse_projection_postulate::
     weak_tarski_s_parallel_postulate::
     weak_triangle_circumscription_principle::
     nil).
Proof.
(* Goal: all_equiv (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) *)
assert(H:=bachmann_s_lotschnittaxiom__weak_inverse_projection_postulate).
(* Goal: all_equiv (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) *)
assert(I:=weak_inverse_projection_postulate__bachmann_s_lotschnittaxiom).
(* Goal: all_equiv (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) *)
assert(J:=weak_inverse_projection_postulate__weak_tarski_s_parallel_postulate).
(* Goal: all_equiv (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) *)
assert(K:=weak_tarski_s_parallel_postulate__weak_inverse_projection_postulate).
(* Goal: all_equiv (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) *)
assert(L:=bachmann_s_lotschnittaxiom__weak_triangle_circumscription_principle).
(* Goal: all_equiv (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) *)
assert(M:=weak_triangle_circumscription_principle__bachmann_s_lotschnittaxiom).
(* Goal: all_equiv (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) *)
apply all_equiv__equiv; unfold all_equiv, all_equiv' in *; simpl in *; tauto.
Qed.

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.
(* Goal: stronger (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop)))))) *)
assert(HPPWC1:=equivalent_postulates_without_any_continuity).
(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
assert(HPPWC2:=equivalent_postulates_without_any_continuity_bis).
(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
assert(H:=thales_converse_postulate__weak_triangle_circumscription_principle).
(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
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).
(* Goal: stronger (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) (@app Prop (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop)))))) *)
apply stronger2__stronger_right; trivial.
(* Goal: stronger (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)) *)
eapply stronger_transitivity; eauto; [|discriminate].
(* Goal: stronger (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)) *)
apply all_equiv2_impl__stronger with bachmann_s_lotschnittaxiom legendre_s_parallel_postulate; simpl; auto.
(* Goal: all_equiv (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)) *)
apply all_equiv_trivial.
Qed.

Theorem equivalent_postulates_assuming_archimedes_axiom :
  archimedes_axiom ->
  all_equiv
    (alternate_interior_angles_postulate::
     alternative_playfair_s_postulate::
     alternative_proclus_postulate::
     alternative_strong_parallel_postulate::
     bachmann_s_lotschnittaxiom::
     consecutive_interior_angles_postulate::
     euclid_5::
     euclid_s_parallel_postulate::
     existential_playfair_s_postulate::
     existential_thales_postulate::
     inverse_projection_postulate::
     legendre_s_parallel_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::
     weak_inverse_projection_postulate::
     weak_tarski_s_parallel_postulate::
     weak_triangle_circumscription_principle::
     nil).
Proof.
(* Goal: forall _ : @archimedes_axiom Tn, all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))))))))))))))))))))) *)
intro HA.
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::
  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) ++
  (bachmann_s_lotschnittaxiom::weak_inverse_projection_postulate::weak_tarski_s_parallel_postulate::
  weak_triangle_circumscription_principle::nil) ++
  (legendre_s_parallel_postulate::nil))).

(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))))))))))))))))))))) *)
  {
(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
  assert(H:=thales_converse_postulate__weak_triangle_circumscription_principle).
(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
  assert(I:=bachmann_s_lotschnittaxiom__legendre_s_parallel_postulate).
(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
  assert(J:=legendre_s_fourth_theorem_aux HA).
(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
  assert(K:=all_equiv_trivial legendre_s_parallel_postulate).
(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
  assert(HPPG:=equivalent_postulates_assuming_greenberg_s_axiom (aristotle__greenberg (t22_24 HA))).
(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
  assert(HPPWC2:=equivalent_postulates_without_any_continuity_bis).
  apply all_equiv3_impl3__all_equiv with thales_converse_postulate
    weak_triangle_circumscription_principle bachmann_s_lotschnittaxiom legendre_s_parallel_postulate
    legendre_s_parallel_postulate postulate_of_right_saccheri_quadrilaterals; trivial; inlist.
  }

(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))))))))))))))))))))) *)
eapply incl_preserves_all_equiv; eauto.
(* Goal: @incl Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
clear HA He; intros a H; repeat induction H; inlist.
Qed.

End Euclid.

Section Euclidean.

(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))))))))))))))))))))) *)
Context `{TE:Tarski_euclidean}.

Lemma inter_dec : forall A B C D,
  (exists I, Col I A B /\ Col I C D) \/ ~ (exists I, Col I A B /\ Col I C D).
Proof.
(* Goal: forall A B C D : @Tpoint Tn, or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I A B) (@Col Tn I C D))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I A B) (@Col Tn I C D)))) *)
apply strong_parallel_postulate_implies_inter_dec.
(* Goal: @strong_parallel_postulate Tn *)
cut tarski_s_parallel_postulate.
(* Goal: forall _ : @tarski_s_parallel_postulate Tn, @strong_parallel_postulate Tn *)
(* Goal: @tarski_s_parallel_postulate Tn *)
apply equivalent_postulates_without_decidability_of_intersection_of_lines_bis; simpl; inlist.
(* Goal: @tarski_s_parallel_postulate Tn *)
(* Goal: @decidability_of_intersection Tn *)
(* Goal: forall (P Q A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Acute Tn A B C), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
unfold tarski_s_parallel_postulate; apply euclid.
Qed.

Lemma aristotle : forall P Q A B C, ~ Col A B C -> Acute A B C ->
  exists X Y, Out B A X /\ Out B C Y /\ Per B X Y /\ Lt P Q X Y.
Proof.
(* Goal: forall (P Q A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Acute Tn A B C), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
assert (H : aristotle_s_axiom).
(* Goal: @aristotle_s_axiom Tn *)
(* Goal: forall (P Q A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Acute Tn A B C), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
cut decidability_of_intersection.
apply (equivalence_of_aristotle_greenberg_and_decidability_of_intersection tarski_s_parallel_postulate);
  [simpl; inlist..|].
(* Goal: @tarski_s_parallel_postulate Tn *)
(* Goal: @decidability_of_intersection Tn *)
(* Goal: forall (P Q A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Acute Tn A B C), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
unfold tarski_s_parallel_postulate; apply euclid.
(* Goal: @decidability_of_intersection Tn *)
(* Goal: forall (P Q A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Acute Tn A B C), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
unfold decidability_of_intersection; apply inter_dec.
(* Goal: forall (P Q A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Acute Tn A B C), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (and (@Per Tn B X Y) (@Lt Tn P Q X Y))))) *)
apply H.
Qed.

Lemma greenberg : forall P Q R A B C, ~ Col A B C ->
  Acute A B C -> Q <> R -> Per P Q R ->
  exists S, LtA P S Q A B C /\ Out Q S R.
Proof.
(* Goal: forall (P Q R A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Acute Tn A B C) (_ : not (@eq (@Tpoint Tn) Q R)) (_ : @Per Tn P Q R), @ex (@Tpoint Tn) (fun S : @Tpoint Tn => and (@LtA Tn P S Q A B C) (@Out Tn Q S R)) *)
apply aristotle__greenberg.
(* Goal: @aristotle_s_axiom Tn *)
unfold aristotle_s_axiom; apply aristotle.
Qed.

Theorem postulates_in_euclidean_context : forall P, List.In P
    (alternate_interior_angles_postulate::
     alternative_playfair_s_postulate::
     alternative_proclus_postulate::
     alternative_strong_parallel_postulate::
     bachmann_s_lotschnittaxiom::
     consecutive_interior_angles_postulate::
     euclid_5::
     euclid_s_parallel_postulate::
     existential_playfair_s_postulate::
     existential_thales_postulate::
     inverse_projection_postulate::
     legendre_s_parallel_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::
     weak_inverse_projection_postulate::
     weak_tarski_s_parallel_postulate::
     weak_triangle_circumscription_principle::
     nil) ->
     P.
Proof.
assert (Haux : forall P, List.In P
  (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) -> P).

(* Goal: all_equiv (@app Prop (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@nil Prop)))))))))))))))))))))))))))))))) (@app Prop (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))) (@cons Prop (@legendre_s_parallel_postulate Tn) (@nil Prop)))) *)
(* Goal: all_equiv (@cons Prop (@alternate_interior_angles_postulate Tn) (@cons Prop (@alternative_playfair_s_postulate Tn) (@cons Prop (@alternative_proclus_postulate Tn) (@cons Prop (@alternative_strong_parallel_postulate Tn) (@cons Prop (@bachmann_s_lotschnittaxiom Tn) (@cons Prop (@consecutive_interior_angles_postulate Tn) (@cons Prop (@euclid_5 Tn) (@cons Prop (@euclid_s_parallel_postulate Tn) (@cons Prop (@existential_playfair_s_postulate Tn) (@cons Prop (@existential_thales_postulate Tn) (@cons Prop (@inverse_projection_postulate Tn) (@cons Prop (@legendre_s_parallel_postulate Tn) (@cons Prop (@midpoint_converse_postulate Tn) (@cons Prop (@perpendicular_transversal_postulate Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@playfair_s_postulate Tn) (@cons Prop (@posidonius_postulate Tn) (@cons Prop (@universal_posidonius_postulate Tn) (@cons Prop (@postulate_of_existence_of_a_right_lambert_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_right_saccheri_quadrilateral Tn) (@cons Prop (@postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn) (@cons Prop (@postulate_of_existence_of_similar_triangles Tn) (@cons Prop (@postulate_of_parallelism_of_perpendicular_transversals Tn) (@cons Prop (@postulate_of_right_lambert_quadrilaterals Tn) (@cons Prop (@postulate_of_right_saccheri_quadrilaterals Tn) (@cons Prop (@postulate_of_transitivity_of_parallelism Tn) (@cons Prop (@proclus_postulate Tn) (@cons Prop (@strong_parallel_postulate Tn) (@cons Prop (@tarski_s_parallel_postulate Tn) (@cons Prop (@thales_postulate Tn) (@cons Prop (@thales_converse_postulate Tn) (@cons Prop (@triangle_circumscription_principle Tn) (@cons Prop (@triangle_postulate Tn) (@cons Prop (@weak_inverse_projection_postulate Tn) (@cons Prop (@weak_tarski_s_parallel_postulate Tn) (@cons Prop (@weak_triangle_circumscription_principle Tn) (@nil Prop))))))))))))))))))))))))))))))))))))) *)
  {
  intros P H.
  cut tarski_s_parallel_postulate; [|unfold tarski_s_parallel_postulate; apply euclid].
  assert (G := greenberg).
  apply (equivalent_postulates_assuming_greenberg_s_axiom G); [assumption|inlist].
  }

intros P H.
assert (HP : List.In P (
  (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) ++
  (legendre_s_parallel_postulate::bachmann_s_lotschnittaxiom::weak_inverse_projection_postulate::
  weak_tarski_s_parallel_postulate::weak_triangle_circumscription_principle::nil)))
by (clear Haux; unfold List.In in *; repeat induction H; inlist).
clear H.
apply in_app_or in HP.
destruct HP as [HP|HP]; [apply Haux, HP|].
cut existential_thales_postulate.
  clear Haux; apply stronger_postulates_ter; [inlist|assumption].
  clear dependent P; apply Haux; inlist.
Qed.

End Euclidean.