proposition: Lemma cop_npar__inter : forall A1 B1 A2 B2, A1 <> B1 -> A2 <> B2 -> Coplanar A1 B1 A2 B2 -> ~ Par A1 B1 A2 B2 -> exists X, Inter A1 B1 A2 B2 X.
proof: Proof. intros. destruct (cop_npar__inter_exists A1 B1 A2 B2) as [X []]. assumption. assumption. exists X. split. assumption. split. induction (col_dec A2 A1 B1). exists B2. split. Col. intro. apply H2. right. repeat split; ColR. exists A2. split; Col. split; Col. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID