proposition: Lemma carre_scalaire_somme : forall A B C D : PO, scalaire (add_PP (vec A B) (vec C D)) (add_PP (vec A B) (vec C D)) = 2 * scalaire (vec A B) (vec C D) + (scalaire (vec A B) (vec A B) + scalaire (vec C D) (vec C D)) :>R.
proof: Proof. intros. VReplace (add_PP (vec A B) (vec C D)) (add_PP (mult_PP 1 (vec A B)) (mult_PP 1 (vec C D))). Simplscal. rewrite (scalaire_sym C D A B); ring. Qed.