proposition: Lemma determinant_nul_alignement : forall A B M : PO, det (vec A B) (vec A M) = 0 -> alignes A B M.
proof: Proof. intros. discrimine A B. elim determinant_nul_colinearite with (A := A) (B := B) (C := A) (D := M); [ intros k H1; try clear determinant_nul_colinearite; try exact H1 | auto | auto ]. apply colineaire_alignes with k; auto. Qed.