proposition: 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: Proof. intros. assert (H:=existential_saccheri__rah). assert (I:=existential_triangle__rah). assert (J:=posidonius_postulate__rah). assert (K:=rah__existential_saccheri). assert (L:=rah__rectangle_principle). assert (M:=rah__similar). assert (N:=rah__thales_postulate). assert (O:=rah__triangle). assert (P:=rah__posidonius). assert (Q:=rectangle_existence__rah). assert (R:=rectangle_principle__rectangle_existence). assert (S:=similar__rah). assert (T:=thales_converse_postulate__thales_existence). assert (U:=thales_existence__rah). assert (V:=thales_postulate__thales_converse_postulate). assert (W:=triangle__existential_triangle). apply all_equiv__equiv; unfold all_equiv'; simpl; repeat (split; tauto). Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.SPP_tarski GeoCoq.Meta_theory.Parallel_postulates.alternate_interior_angles_consecutive_interior_angles GeoCoq.Meta_theory.Parallel_postulates.alternate_interior_angles_playfair_bis GeoCoq.Meta_theory.Parallel_postulates.alternate_interior_angles_triangle GeoCoq.Meta_theory.Parallel_postulates.alternate_interior_angles_proclus GeoCoq.Meta_theory.Parallel_postulates.bachmann_s_lotschnittaxiom_legendre_s_parallel_postulate GeoCoq.Meta_theory.Parallel_postulates.bachmann_s_lotschnittaxiom_weak_inverse_projection_postulate GeoCoq.Meta_theory.Parallel_postulates.bachmann_s_lotschnittaxiom_weak_triangle_circumscription_principle GeoCoq.Meta_theory.Parallel_postulates.consecutive_interior_angles_alternate_interior_angles GeoCoq.Meta_theory.Parallel_postulates.existential_playfair_rah GeoCoq.Meta_theory.Parallel_postulates.existential_saccheri_rah GeoCoq.Meta_theory.Parallel_postulates.inverse_projection_postulate_proclus_bis GeoCoq.Meta_theory.Parallel_postulates.legendre GeoCoq.Meta_theory.Parallel_postulates.midpoint_playfair GeoCoq.Meta_theory.Parallel_postulates.original_euclid_original_spp GeoCoq.Meta_theory.Parallel_postulates.original_spp_inverse_projection_postulate GeoCoq.Meta_theory.Parallel_postulates.par_perp_2_par_par_perp_perp GeoCoq.Meta_theory.Parallel_postulates.par_perp_perp_par_perp_2_par GeoCoq.Meta_theory.Parallel_postulates.par_perp_perp_playfair GeoCoq.Meta_theory.Parallel_postulates.par_trans_playfair GeoCoq.Meta_theory.Parallel_postulates.playfair_existential_playfair GeoCoq.Meta_theory.Parallel_postulates.playfair_midpoint GeoCoq.Meta_theory.Parallel_postulates.playfair_par_trans GeoCoq.Meta_theory.Parallel_postulates.posidonius_postulate_rah GeoCoq.Meta_theory.Parallel_postulates.proclus_aristotle GeoCoq.Meta_theory.Parallel_postulates.proclus_bis_proclus GeoCoq.Meta_theory.Parallel_postulates.rah_existential_saccheri GeoCoq.Meta_theory.Parallel_postulates.rah_rectangle_principle GeoCoq.Meta_theory.Parallel_postulates.rah_similar GeoCoq.Meta_theory.Parallel_postulates.rah_thales_postulate GeoCoq.Meta_theory.Parallel_postulates.rah_posidonius_postulate GeoCoq.Meta_theory.Parallel_postulates.rectangle_existence_rah GeoCoq.Meta_theory.Parallel_postulates.rectangle_principle_rectangle_existence GeoCoq.Meta_theory.Parallel_postulates.similar_rah GeoCoq.Meta_theory.Parallel_postulates.tarski_playfair GeoCoq.Meta_theory.Parallel_postulates.thales_converse_postulate_thales_existence GeoCoq.Meta_theory.Parallel_postulates.thales_converse_postulate_weak_triangle_circumscription_principle GeoCoq.Meta_theory.Parallel_postulates.thales_existence_rah GeoCoq.Meta_theory.Parallel_postulates.thales_postulate_thales_converse_postulate GeoCoq.Meta_theory.Parallel_postulates.weak_inverse_projection_postulate_bachmann_s_lotschnittaxiom GeoCoq.Meta_theory.Parallel_postulates.weak_inverse_projection_postulate_weak_tarski_s_parallel_postulate GeoCoq.Meta_theory.Parallel_postulates.weak_tarski_s_parallel_postulate_weak_inverse_projection_postulate GeoCoq.Meta_theory.Parallel_postulates.weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom GeoCoq.Tarski_dev.Annexes.saccheri GeoCoq.Tarski_dev.Annexes.perp_bisect GeoCoq.Tarski_dev.Annexes.quadrilaterals GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Utils.all_equiv Rtauto