Equitable functions #
This file defines equitable functions.
f is equitable on a set
f a₁ ≤ f a₂ + 1 for all
a₁, a₂ ∈ s. This is mostly
useful when the codomain of
ℤ (or more generally a successor order).
ℕ can be replaced by any
conditionally_complete_monoid, but we don't have the