proposition: Lemma max_elt_spec2 : forall (s : t) (x y : elt) (Hs : Ok s), max_elt s = Some x -> In y s -> ~ X.lt x y.
proof: Proof. induction s as [ | a s IH]. - inversion 2. - destruct s as [ | b s]. + inversion 2; subst. intros; inv; order. + intros. inv; auto. assert (~X.lt x b) by (apply IH; auto). assert (X.lt a b) by auto. order. Qed.
imports: MSetInterface OrdersFacts OrdersLists