proposition: Lemma min_elt_spec2 : forall (s : t) (x y : elt) (Hs : Ok s), min_elt s = Some x -> In y s -> ~ X.lt y x.
proof: Proof. induction s as [ | x s IH]; simpl; inversion 2; subst. intros; inv; try sort_inf_in; order. Qed.
imports: MSetInterface OrdersFacts OrdersLists