proposition: Lemma not_par_strict_inter_exists : forall A1 B1 A2 B2, ~Par_strict A1 B1 A2 B2 -> exists X, Col X A1 B1 /\ Col X A2 B2.
proof: Proof. intros A1 B1 A2 B2. apply (cop_npars__inter_exists). apply all_coplanar. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID