proposition: Lemma compare_spec : forall s s' : t, CompSpec eq lt s s' (compare s s').
proof: Proof. intros. case_eq (compare s s'); intro H; constructor. - apply compare_eq, H. - assumption. - apply compare_gt, H. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface