proposition: Lemma playfair__playfair_quater : playfair_s_postulate -> playfair_quater.
proof: Proof. intro HP; intro HPQ; destruct HPQ as [A1 [A2 [B1 [B2 [C1 [C2 [P HPQ]]]]]]]. assert (H:= HP A1 A2 B1 B2 C1 C2 P); clear HP. destruct HPQ as [HD1 [HD2 [HD3 [HC1 [HC2 [HNC1 [HNC2 [HNC3 HPQ]]]]]]]]. destruct HPQ as [HIAB [HIAC [HNI1 HNI2]]]. apply HNC3; apply H; clear H; Col; left; repeat (split; try assumption); auto. { destruct HIAB as [IAB HIAB]; exists IAB. clear HD1 HD2 HD3 HC1 HC2 HNC1 HNC2 HNC3 HIAC HNI1 HNI2 P C1 C2. induction (col2_dec A1 A2 IAB B1 B2 IAB). left; assumption. induction (col2_dec A1 B1 IAB A2 B2 IAB). right; left; assumption. induction (col2_dec A1 B2 IAB A2 B1 IAB). right; right; assumption. exfalso; apply HIAB; repeat split; assumption. } { destruct HIAC as [IAC HIAC]; exists IAC. clear HD1 HD2 HD3 HC1 HC2 HNC1 HNC2 HNC3 HIAB HNI1 HNI2 P B1 B2. induction (col2_dec A1 A2 IAC C1 C2 IAC). left; assumption. induction (col2_dec A1 C1 IAC A2 C2 IAC). right; left; assumption. induction (col2_dec A1 C2 IAC A2 C1 IAC). right; right; assumption. exfalso; apply HIAC; repeat split; assumption. } Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Ch12_parallel