proposition: Lemma playfair_quater__playfair : playfair_quater -> playfair_s_postulate.
proof: Proof. intros HP A1 A2 B1 B2 C1 C2 P HPar1 HP1 HPar2 HP2. assert (H : playfair_quater <-> forall A1 A2 B1 B2 C1 C2 P, ~ playfair_quater_qf A1 A2 B1 B2 C1 C2 P) by (apply not_ex_forall_not_7). rewrite H in HP; clear H. assert (H : Col C1 B1 B2 /\ Col C2 B1 B2 <-> ~ ~ (Col C1 B1 B2 /\ Col C2 B1 B2)) by (induction (col_dec C1 B1 B2); induction (col_dec C2 B1 B2); tauto). apply H; clear H; intro HNC; apply (HP A1 A2 B1 B2 C1 C2 P). assert_diffs. repeat (split; [assumption|]). assert (HNC1 : ~ Col A1 B1 B2). { intro. apply (not_strict_par _ _ _ _ A1) in HPar1; Col; spliter. apply (not_strict_par _ _ _ _ P) in HPar2; spliter; [apply HNC; split|..]; ColR. } assert (HNC2 : ~ Col A1 C1 C2). { intro. apply (not_strict_par _ _ _ _ A1) in HPar2; Col; spliter. apply (not_strict_par _ _ _ _ P) in HPar1; spliter; [apply HNC; split|..]; ColR. } apply par_symmetry in HPar1; apply (par_not_col_strict _ _ _ _ A1) in HPar1; Col; apply par_strict_symmetry in HPar1; destruct HPar1 as [HCop1 HPar1]. apply par_symmetry in HPar2; apply (par_not_col_strict _ _ _ _ A1) in HPar2; Col; apply par_strict_symmetry in HPar2; destruct HPar2 as [HCop2 HPar2]. repeat (split; [tauto|]); intuition. { destruct HCop1 as [IAB HIAB]. exists IAB; intros [HIAB1 [HIAB2 HIAB3]]. elim HIAB; clear HIAB; intro HIAB. apply HIAB1; spliter; split; Col. elim HIAB; clear HIAB; intro HIAB; [apply HIAB2|apply HIAB3]; spliter; split; Col. } { destruct HCop2 as [IAC HIAC]. exists IAC; intros [HIAC1 [HIAC2 HIAC3]]. elim HIAC; clear HIAC; intro HIAC. apply HIAC1; spliter; split; Col. elim HIAC; clear HIAC; intro HIAC; [apply HIAC2|apply HIAC3]; spliter; split; Col. } Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Ch12_parallel