proposition: Lemma max_elt_spec3 : forall s : t, max_elt s = None -> Empty s.
proof: Proof. induction s as [ | a s IH]. - red; intuition; inv. - destruct s as [ | b s]. + inversion 1. + intros; elim IH with b; auto. Qed.
imports: MSetInterface OrdersFacts OrdersLists