proposition: Lemma existence_mediatrice : forall A B : PO, A <> B :>PO -> ex (fun J : PO => milieu A B <> J :>PO /\ mediatrice A B J).
proof: Proof. intros. soit_milieu A B M. soit_orthogonal M A J. exists J. split; [ try assumption | idtac ]. apply orthogonale_segment_milieu_mediatrice with M; auto. apply orthogonal_milieu with M; auto. Qed.