proposition: Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
proof: Proof. intros x y. unfold compare. case_eq (x <=? y). - case_eq (y <=? x). + constructor. split; auto. + constructor. split; congruence. - constructor. destruct (leb_total x y); split; congruence. Qed.
imports: Relations Morphisms Setoid Equalities