proposition: Lemma choose_spec3 : forall s s' x x' `{Ok s, Ok s'}, choose s = Some x -> choose s' = Some x' -> Equal s s' -> X.eq x x'.
proof: Proof. unfold choose, Equal; intros s s' x x' Hb Hb' Hx Hx' H. assert (~X.lt x x'). { apply min_elt_spec2 with s'; auto. rewrite <-H; auto using min_elt_spec1. } assert (~X.lt x' x). { apply min_elt_spec2 with s; auto. rewrite H; auto using min_elt_spec1. } elim_compare x x'; intuition. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat