proposition: Lemma milieu_vecteur2 : forall A B M : PO, M = milieu A B :>PO -> vec A M = mult_PP (/ 2) (vec A B) :>PP.
proof: Proof. intros; unfold vec in |- *. cut (2 <> 0); intros; auto with real. apply mult_PP_regulier with 2; auto. replace (mult_PP 2 (add_PP (cons (-1) A) (cons 1 M))) with (add_PP (cons (-2) A) (cons 2 M)). rewrite H; rewrite <- add_PP_milieu. FieldPP 2. RingPP. Qed.