proposition: Lemma max_elt_spec3 s : max_elt s = None -> Empty s.
proof: Proof. induction s as [|t1 s1 IHs1 x s2 IHs2]; simpl in *; intros H. + inversion 1. + destruct s2 as [|? ? y]; [congruence|]. destruct (IHs2 H y); auto. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat