proposition: Lemma max_elt_spec1 s x : max_elt s = Some x -> InT x s.
proof: Proof. induction s as [|t1 s1 IHs1 y [|] IHs2]; simpl in *; intros H; [congruence| |auto]. replace y with x by congruence; auto. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat