proposition: Lemma scalaire_bilineaire : forall (a b c d : R) (A B C D E F G H : PO), scalaire (add_PP (mult_PP a (vec A B)) (mult_PP b (vec C D))) (add_PP (mult_PP c (vec E F)) (mult_PP d (vec G H))) = a * c * scalaire (vec A B) (vec E F) + a * d * scalaire (vec A B) (vec G H) + (b * c * scalaire (vec C D) (vec E F) + b * d * scalaire (vec C D) (vec G H)).
proof: Proof. intros a b c d A B C D E F G I; try assumption. elim existence_representant_comb_lin_vecteur with (A := E) (B := F) (C := G) (D := I) (a := c) (b := d); intros E0 H; try clear existence_representant_comb_lin_vecteur; rewrite <- H. rewrite scalaire_lineaire_g. rewrite H. repeat rewrite scalaire_lineaire_d. ring. Qed.