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; intros s s' x x' Hs Hs' 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. } order. Qed.
imports: MSetInterface OrdersFacts OrdersLists