proposition: Lemma milieu_distinct : forall A B : PO, A <> B :>PO -> A <> milieu A B :>PO.
proof: Proof. intros A B H; try assumption. apply distinct_produit_vecteur with (B := B) (a := / 2); auto with real. rewrite <- (milieu_vecteur2 (A:=A) (B:=B) (M:=milieu A B)); auto. Qed.