proposition: Lemma parallel_uniqueness : forall A1 A2 B1 B2 C1 C2 P : Tpoint, Par A1 A2 B1 B2 -> Col P B1 B2 -> Par A1 A2 C1 C2 -> Col P C1 C2 -> Col C1 B1 B2 /\ Col C2 B1 B2.
proof: Proof. apply tarski_s_euclid_implies_playfair. unfold tarski_s_parallel_postulate; apply euclid. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID