proposition: Lemma scalaire_mult_d : forall (k : R) (A B C D : PO), scalaire (vec A B) (mult_PP k (vec C D)) = k * scalaire (vec A B) (vec C D) :>R.
proof: Proof. intros. replace (mult_PP k (vec C D)) with (add_PP (mult_PP k (vec C D)) (mult_PP 0 (vec C D))). rewrite scalaire_lineaire_d. ring. unfold vec in |- *; RingPP. Qed.