proposition: Lemma deux_milieux_distincts : forall A B C I J : PO, A <> C :>PO -> I = milieu A B :>PO -> J = milieu B C :>PO -> I <> J :>PO.
proof: Proof. intros. lapply (droite_milieu (A:=B) (B:=A) (C:=C) (I:=I) (J:=J)); auto with geo; intros. contrapose H. apply vecteur_nul_conf. rewrite <- H2; auto. rewrite <- H3; Ringvec. Qed.