proposition: Lemma max_elt_spec1 : forall (s : t) (x : elt), max_elt s = Some x -> In x s.
proof: Proof. induction s as [ | x s IH]. - inversion 1. - destruct s as [ | y s]. + simpl. inversion 1; subst; auto. + right; apply IH; auto. Qed.
imports: MSetInterface OrdersFacts OrdersLists