proposition: Lemma par_trans_implies_playfair : postulate_of_transitivity_of_parallelism -> playfair_s_postulate.
proof: Proof. intros HPT A1; intros. assert (Par C1 C2 B1 B2) by (apply HPT with A1 A2; Par). induction H3. exfalso; apply H3; exists P; Col. spliter; split; Col. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Ch12_parallel