proposition: Theorem position_relative_droites_coplanaires : forall A B C D : PO, A <> B :>PO -> C <> D :>PO -> coplanaires A B C D -> concours (droite A B) (droite C D) \/ paralleles (droite A B) (droite C D).
proof: Proof. intros A B C D H10 H H0; try assumption. elim position_relative_droites_espace with (A := A) (B := B) (C := C) (D := D); [ intros H1; try clear position_relative_droites_espace | intros H1; try clear position_relative_droites_espace; auto | auto | auto ]. absurd (coplanaires A B C D); auto. Qed.