proposition: Lemma alternate_interior__playfair_bis : alternate_interior_angles_postulate -> alternative_playfair_s_postulate.
proof: Proof. intros aia. intros A1 A2 B1 B2 C1 C2 P HPerp2 HPB HCop HParAC HPC. split. apply (alternate_interior__playfair_aux aia A1 A2 _ _ _ C2 P); auto. apply (alternate_interior__playfair_aux aia A1 A2 _ _ _ C1 P); Col; Par. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Ch13_1