proposition: Lemma cop_par__inter : forall A B C D P Q, Par A B C D -> ~Par A B P Q -> Coplanar C D P Q -> exists Y, Col P Q Y /\ Col C D Y.
proof: Proof. intros A B C D P Q HPar HNPar HCop. destruct (cop_npar__inter_exists C D P Q) as [Y []]. assumption. intro. apply HNPar, par_trans with C D; assumption. exists Y; split; Col. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID