proposition: Lemma symetrie_milieu : forall A B I : PO, B = symetrie I A :>PO -> I = milieu A B :>PO.
proof: Proof. unfold symetrie in |- *; intros. cut (vec I B = mult_PP (-1) (vec I A)); intros. 2: apply homothetie_vecteur; auto. apply vecteur_milieu. replace (vec A B) with (add_PP (vec A I) (vec I B)); [ idtac | Ringvec ]. rewrite H0. cut (2 <> 0); intros; auto with real. Fieldvec 2. Qed.