proposition: Lemma compare_spec x y : CompSpec eq lt x y (compare x y).
proof: Proof. unfold compare; repeat destruct eq_dec; auto; constructor. - destruct (lt_total x y); auto. absurd (x==y); auto. transitivity (max x y); auto. symmetry. apply max_l. rewrite le_lteq; intuition. - destruct (lt_total y x); auto. absurd (max x y == y); auto. apply max_r; rewrite le_lteq; intuition auto with relations. Qed.
imports: Orders OrdersTac OrdersFacts Setoid Morphisms Basics