proposition: Lemma existence_symetrique_milieu: forall (A I : PO), (exists B : PO , I = milieu A B ).
proof: Proof. intros. elim (existence_symetrique I A); [intros B H; (try clear existence_symetrique); (try exact H)]. exists B. apply symetrie_milieu; auto. Qed.