proposition: Lemma playfair_ter__playfair : playfair_ter -> playfair_s_postulate.
proof: Proof. intros HP A1 A2 B1 B2 C1 C2 P HPar1 HP1 HPar2 HP2. elim (col_dec A1 B1 B2); intro HNC1. { assert (HA : A1 <> A2) by (assert_diffs; auto). assert (HB : B1 <> B2) by (assert_diffs; auto). assert (HC : C1 <> C2) by (assert_diffs; auto). apply (not_strict_par _ _ _ _ A1) in HPar1; Col. destruct HPar1 as [HC1 HC2]; clear HNC1. apply (not_strict_par _ _ _ _ P) in HPar2; spliter; [split|..]; ColR. } { elim (col_dec A1 C1 C2); intro HNC2. { assert (HA : A1 <> A2) by (assert_diffs; auto). assert (HB : B1 <> B2) by (assert_diffs; auto). assert (HC : C1 <> C2) by (assert_diffs; auto). apply (not_strict_par _ _ _ _ A1) in HPar2; Col. destruct HPar2 as [HC1 HC2]; clear HNC2. apply (not_strict_par _ _ _ _ P) in HPar1; spliter; [split|..]; ColR. } { 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); intuition). assert_diffs; apply H; clear H; intro HNC3; apply (HP A1 A2 B1 B2 C1 C2 P); Col; try (intros [HC1 HC2]; auto). { apply par_symmetry in HPar1. apply (par_not_col_strict _ _ _ _ A1) in HPar1; Col. destruct HPar1 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. } { apply par_symmetry in HPar2. apply (par_not_col_strict _ _ _ _ A1) in HPar2; Col. destruct HPar2 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. } { apply par_symmetry in HPar1; apply par_symmetry in HPar2. apply (par_not_col_strict _ _ _ _ A1) in HPar1; Col. apply (par_not_col_strict _ _ _ _ A1) in HPar2; Col. destruct HPar1 as [_ HI1]; destruct HPar2 as [_ HI2]. split; intros [I [HC1 HC2]]; [apply HI1|apply HI2]; exists I; Col. } } } Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Ch12_parallel