proposition: Lemma expr_compare_spec: forall x y, compare_spec (x=y) (expr_compare x y).
proof: Proof. induction x; destruct y; try (constructor; congruence). - eapply lex_spec; eauto. intuition congruence. - eapply lex_spec; eauto. intuition congruence. - simpl; case IHx; constructor; congruence. - simpl; case cmp_spec; constructor; congruence. Qed.
imports: positives comparisons lattice lset sups