proposition: Lemma scalaire_difference_carre : forall A B I M : PO, I = milieu A B -> scalaire (vec M A) (vec M B) = Rsqr (distance M I) + - Rsqr (distance I A).
proof: Proof. intros. unfold Rsqr in |- *; repeat rewrite <- carre_scalaire_distance. VReplace (vec M B) (add_PP (mult_PP 1 (vec M I)) (mult_PP 1 (vec I B))). rewrite <- (milieu_vecteur H); auto. VReplace (mult_PP 1 (vec A I)) (mult_PP (-1) (vec I A)). VReplace (vec M A) (add_PP (mult_PP 1 (vec M I)) (mult_PP 1 (vec I A))). Simplscal. rewrite (scalaire_sym M I I A); ring. Qed.