proposition: Lemma par_perp_2_par_implies_par_perp_perp : postulate_of_parallelism_of_perpendicular_transversals -> perpendicular_transversal_postulate.
proof: Proof. intros HPPP A B C D P Q HPar HPerp HCop. elim HPar; clear HPar; intro HPar; [|spliter; apply perp_col2 with A B; auto; ColR]. assert (HX := HPerp); destruct HX as [X HX]. elim (col_dec C D X); intro HCDX. exfalso; apply HPar; exists X; unfold Perp_at in HX; spliter; Col. assert (HY := l8_18_existence C D X HCDX); destruct HY as [Y [HCDY HPerp']]. assert (HPar' : Par P Q X Y). { destruct HX as [_ [_ [HCol [ ]]]]; assert_diffs. assert (Coplanar C D X A) by (apply col2_cop__cop with A B; Col; apply pars__coplanar; Par). assert (Coplanar C D X B) by (apply col2_cop__cop with A B; Col; apply pars__coplanar; Par). assert (Coplanar C D X P) by (apply col2_cop__cop with P Q; Col; apply perp__coplanar; Perp). assert (Coplanar C D X Q) by (apply col2_cop__cop with P Q; Col; apply perp__coplanar; Perp). assert (Coplanar C D X Y) by Cop. apply HPPP with A B C D; Perp; try solve [left; auto]; try solve [apply col2_cop__cop with P Q; Col; Cop]; CopR. } elim HPar'; clear HPar'; intro HPar'. exfalso; apply HPar'; exists X; unfold Perp_at in HX; spliter; Col. destruct HPar' as [HPQ [HXY [HCol1 HCol2]]]. apply perp_sym; apply perp_col2 with X Y; Col; Perp. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Ch12_parallel