proposition: Lemma not_par_inter : forall A B A' B' X Y, ~Par A B A' B' -> (exists P, Col P X Y /\ (Col P A B \/ Col P A' B')).
proof: Proof. intros. assert (HC := all_coplanar). apply (cop2_npar__inter); auto. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID