proposition: Lemma milieu_distance : forall A B I : PO, I = milieu A B -> distance I A = distance I B.
proof: Proof. intros. apply carre_scalaire_egalite_distance. rewrite <- (milieu_vecteur (A:=A) (B:=B) (M:=I)); auto with geo. replace (vec I A) with (mult_PP (-1) (vec A I)); [ idtac | Ringvec ]. Simplscal. Qed.