proposition: Lemma par_perp_perp_implies_playfair : perpendicular_transversal_postulate -> playfair_s_postulate.
proof: Proof. intro HPTP; intros A1 A2 B1 B2 C1 C2 P HPar1 HCol1. revert C1 C2. cut (forall C1 C2, P <> C1 -> Par A1 A2 C1 C2 -> Col P C1 C2 -> Col C1 B1 B2 /\ Col C2 B1 B2). { intros Haux C1 C2. elim (eq_dec_points P C1); auto. intro HC1. elim (eq_dec_points P C2); intros HC2 HPar2 HCol2. subst; split; assumption. elim (Haux C2 C1); Col; Par. } intros C1 C2 HDiff HPar2 HCol2. elim (col_dec A1 A2 P); intro HCol. { elim HPar1; clear HPar1; intro HPar1. exfalso; apply HPar1; exists P; split; Col. elim HPar2; clear HPar2; intro HPar2. exfalso; apply HPar2; exists P; split; Col. destruct HPar1 as [_ [HDiff2 [HCol3 HCol4]]]; destruct HPar2 as [HDiff1 [HDiff3 [HCol5 HCol6]]]. split; ColR. } { assert(HI := l8_18_existence A1 A2 P HCol); destruct HI as [I [HCol' HPerp]]. assert (HCop1 : Coplanar B1 B2 P I) by (apply col__coplanar; Col). assert (HCop2 : Coplanar C1 C2 P I) by (apply col__coplanar; Col). assert (HPerp1 := HPTP A1 A2 B1 B2 P I HPar1 HPerp HCop1). assert (HPerp2 := HPTP A1 A2 C1 C2 P I HPar2 HPerp HCop2). assert (HCop3 : Coplanar A1 A2 P B1) by (assert_diffs; apply coplanar_perm_1, col_cop__cop with B2; Col; apply par__coplanar, HPar1). assert (HCop4 : Coplanar A1 A2 P B2) by (assert_diffs; apply coplanar_perm_1, col_cop__cop with B1; Col; apply coplanar_perm_1, par__coplanar, HPar1). assert (HCop5 : Coplanar A1 A2 P C1) by (assert_diffs; apply coplanar_perm_1, col_cop__cop with C2; Col; apply par__coplanar, HPar2). assert (HCop6 : Coplanar A1 A2 P I) by Cop. assert (Perp P C1 P I) by (apply perp_left_comm, perp_col with C2; Col). assert (Col P C1 B1). { elim (eq_dec_points P B1); intro HPB1; [subst; Col|]. apply cop_perp2__col with P I; [CopR|assumption|]. apply perp_left_comm, perp_col with B2; Col. } assert (Col P C1 B2). { elim (eq_dec_points P B2); intro HPB2; [subst; Col|]. apply cop_perp2__col with P I; [CopR|assumption|]. apply perp_left_comm, perp_col with B1; Col; Perp. } split; apply (col3 P C1); Col. } Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Ch12_parallel