proposition: Lemma cop2_npar__inter : forall A B A' B' X Y, Coplanar A B X Y -> Coplanar 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. induction(par_dec A B X Y). assert(~ Par A' B' X Y). intro. apply H1. apply(par_trans _ _ X Y); Par. destruct(cop_npar__inter_exists A' B' X Y) as [P []]. assumption. assumption. exists P. split. Col. right. Col. destruct(cop_npar__inter_exists A B X Y) as [P []]. assumption. assumption. exists P. split. Col. left. Col. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID