proposition: Lemma milieu_distinct2 : forall A B : PO, A <> B :>PO -> B <> milieu A B :>PO.
proof: Proof. intros A B H; try assumption. apply distinct_produit_vecteur with (B := A) (a := / 2); auto with real. cut (vec (milieu A B) B = mult_PP (/ 2) (vec A B)); intros. VReplace (vec B (milieu A B)) (mult_PP (-1) (vec (milieu A B) B)). rewrite H0. cut (2 <> 0); intros; auto with real. Fieldvec 2. rewrite <- (milieu_vecteur (A:=A) (B:=B) (M:=milieu A B)); auto. rewrite <- (milieu_vecteur2 (A:=A) (B:=B) (M:=milieu A B)); auto. Qed.