proposition: Lemma inter__npar : forall A1 A2 B1 B2 X, Inter A1 A2 B1 B2 X -> ~ Par A1 A2 B1 B2.
proof: Proof. intros. destruct H as [HA [[P []] []]]. induction 1. apply (par_not_col A1 A2 B1 B2 X); Col. spliter. apply H0, (col3 B1 B2); Col. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID