mathlib

23cf025c - feat(algebra/ordered_sub): define truncated subtraction in general (#8503)

feat(algebra/ordered_sub): define truncated subtraction in general (#8503) * Define and prove properties of truncated subtraction in general * We currently only instantiate it for `nat`. The other types (`multiset`, `finsupp`, `nnreal`, `ennreal`, ...) will be in future PRs. Todo in future PRs: * Provide `has_ordered_sub` instances for all specific cases * Remove the lemmas specific to each individual type Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>