proposition: Lemma unicite_symetrique: forall (A B P : PO), milieu A P = milieu B P -> A = B.
proof: Proof. intros. elim (existence_milieu B P); [intros I H1; (try clear existence_milieu)]. assert (B = symetrie I P). apply milieu_symetrie; auto with geo. rewrite H0. apply milieu_symetrie. rewrite H1. auto with geo. Qed.