proposition: Lemma vec_directeur_paralleles : forall A B C D : PO, A <> B -> C <> D -> vec_directeur (vec A B) (droite C D) -> paralleles (droite A B) (droite C D).
proof: Proof. intros. elim determinant_nul_colinearite with (A := C) (B := D) (C := A) (D := B); [ intros k H4; try clear determinant_nul_colinearite; try exact H4 | auto | auto with geo ]. apply colineaires_paralleles with k; auto. Qed.