proposition: Lemma scalaire_lineaire_g : forall (a b : R) (A B C D E F : PO), scalaire (add_PP (mult_PP a (vec A B)) (mult_PP b (vec C D))) (vec E F) = a * scalaire (vec A B) (vec E F) + b * scalaire (vec C D) (vec E F).
proof: Proof. intros. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := B) (k := a); intros B' H; try clear existence_representant_mult_vecteur; rewrite <- H. elim existence_representant_mult_vecteur with (A := A) (B := C) (C := D) (k := b); intros C' H0; try clear existence_representant_mult_vecteur; rewrite <- H0. rewrite scalaire_somme_g. rewrite H; rewrite H0. repeat rewrite scalaire_mult_g; auto. Qed.