proposition: Lemma determinant_nul_colinearite : forall A B C D : PO, A <> B -> det (vec A B) (vec C D) = 0 -> exists k : _, vec C D = mult_PP k (vec A B).
proof: Proof. intros A B C D H; try assumption. rewrite determinant_aire; intros. apply aire_nulle_colineaires; auto. Qed.