proposition: Lemma determinant_colineaire_l : forall (k : R) (A B C D : PO), det (mult_PP k (vec A B)) (vec C D) = k * det (vec A B) (vec C D).
proof: Proof. intros. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := B) (k := k); [ intros E H1; rewrite <- H1 ]. repeat rewrite determinant_aire. rewrite H1. apply aire_colineaire_l. Qed.