proposition: Lemma determinant_colinearite : forall (k : R) (A B C D : PO), vec C D = mult_PP k (vec A B) -> det (vec A B) (vec C D) = 0.
proof: Proof. intros. repeat rewrite determinant_aire. apply (aire_colinearite H). Qed.