proposition: Lemma triangle__playfair_bis : greenberg_s_axiom -> triangle_postulate -> alternative_playfair_s_postulate.
proof: Proof. intros greenberg triangle. intros A1 A2 B1 B2 C1 C2 P. split. apply (legendre_aux2 greenberg triangle A1 A2 _ _ _ C2 P); auto. apply (legendre_aux2 greenberg triangle A1 A2 _ _ _ C1 P); Par; Col. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch13_1