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