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