proposition: Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
proof: Proof. unfold eq, lt, compare; intros. destruct (O.compare x y) eqn:H; auto. apply CompGt. rewrite compare_sym, H; auto. Qed.
imports: OrderedType Orders