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