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