proposition: Lemma milieu_symetrie : forall A B I : PO, I = milieu A B :>PO -> B = symetrie I A :>PO.
proof: Proof. unfold symetrie in |- *; intros. apply vecteur_homothetie. rewrite <- (milieu_vecteur (A:=A) (B:=B) (M:=I)); auto. Ringvec. Qed.