proposition: Lemma cop_npars__inter_exists : forall A1 B1 A2 B2, Coplanar A1 B1 A2 B2 -> ~ Par_strict A1 B1 A2 B2 -> exists X, Col X A1 B1 /\ Col X A2 B2.
proof: Proof. intros. induction (eq_dec_points A1 B1). subst. exists A2. Col. induction (eq_dec_points A2 B2). subst. exists A1. Col. induction (inter_dec A1 B1 A2 B2). assumption. exfalso. apply H0. split; assumption. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID