proposition: Lemma universal_posidonius_postulate__perpendicular_transversal_postulate : universal_posidonius_postulate -> perpendicular_transversal_postulate.
proof: Proof. intros HP A B C D P Q HPar. revert P Q. cut (forall P Q, Perp A B P Q -> Coplanar C D P Q -> ~ Col A B P -> Perp C D P Q). { intros Haux P Q HPerp HCop. destruct (perp_not_col2 A B P Q HPerp); [|apply perp_right_comm]; apply Haux; Perp; Cop. } intros P Q HPerp HCop HNCol. assert (HH := HPar). destruct HH as [HPars|]; [|spliter; apply (perp_col2 A B); auto; ColR]. assert (HH := HPerp); destruct HH as [R HR]; apply perp_in_col in HR; destruct HR as [HR1 HR2]. destruct (l8_18_existence A B C) as [E [HE1 HE2]]. apply par_strict_not_col_1 with D, HPars. destruct (l8_18_existence A B D) as [G [HG1 HG2]]. apply par_strict_not_col_4 with C, HPars. assert (E <> G). { intro; subst G. assert (Col C D E) by (apply col_cop2_perp2__col with E A B; [Perp..|Col|Cop|Cop]). apply HPars; exists E; split; Col. } assert (Saccheri E C D G). { repeat split. apply perp_per_1, perp_col0 with A B; Perp. apply perp_per_1, perp_col2 with A B; Perp. apply cong_right_commutativity, HP with A B C D; Perp; Col. apply l12_6, par_strict_symmetry, par_strict_col2_par_strict with A B; Par. } assert (P <> Q) by (apply perp_distinct in HPerp; apply HPerp). apply perp_sym, perp_col with R; Col. apply perp_sym. assert (P <> R) by (intro; subst; apply HNCol, HR1). apply par_distinct in HPar; spliter. apply universal_posidonius_postulate__perpendicular_transversal_postulate_aux with E G; trivial. apply perp_col2 with A B; Col; apply perp_sym, perp_left_comm, perp_col with Q; Perp. apply col_cop__cop with Q; trivial. apply (col3 A B); auto. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.rah_thales_postulate GeoCoq.Meta_theory.Parallel_postulates.thales_converse_postulate_weak_triangle_circumscription_principle GeoCoq.Meta_theory.Parallel_postulates.thales_postulate_thales_converse_postulate GeoCoq.Meta_theory.Parallel_postulates.weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom GeoCoq.Meta_theory.Parallel_postulates.bachmann_s_lotschnittaxiom_variant GeoCoq.Tarski_dev.Annexes.saccheri GeoCoq.Tarski_dev.Ch12_parallel