proposition: Lemma playfair__playfair_ter : playfair_s_postulate -> playfair_ter.
proof: Proof. intros HP A1 A2 B1 B2 C1 C2 P HA HB HC HP1 HP2 HNC1 HNC2 HNC3 HIAB HIAC. intros [HAB HAC]. apply HNC3. apply (HP A1 A2 B1 B2 C1 C2 P); Col; left; repeat (split; Col). { destruct HIAB as [IAB HIAB]; exists IAB. clear HA HB HC HP1 HP2 HNC1 HNC2 HNC3 HIAC HAB HAC 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 HA HB HC HP1 HP2 HNC1 HNC2 HNC3 HIAB HAB HAC 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