proposition: Lemma compare_spec : CompSpec eq lt s s' (compare s s').
proof: Proof. unfold compare; destruct (@M.compare_spec s s' _ _); auto. Qed.
imports: Bool SetoidList RelationClasses Morphisms RelationPairs Equalities Orders OrdersFacts