proposition: Lemma par_inter : forall A B C D P Q, Par A B C D -> ~Par A B P Q -> exists Y, Col P Q Y /\ Col C D Y.
proof: Proof. intros. assert (HC := all_coplanar C D P Q). apply (cop_par__inter A B); assumption. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID