proposition: Lemma demi_longueur : forall A B I : PO, I = milieu A B -> Rsqr (distance A B) = R4 * Rsqr (distance A I) :>R.
proof: Proof. intros. unfold Rsqr, R4 in |- *; repeat rewrite <- carre_scalaire_distance. replace (vec A B) with (mult_PP 2 (vec A I)). Simplscal. rewrite <- (milieu_vecteur_double H); auto. Qed.