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