mathlib

f63786b9 - refactor(data/finsupp/basic): has_ordered_sub on finsupp (#9577)

refactor(data/finsupp/basic): has_ordered_sub on finsupp (#9577) * Generalize `has_sub` and `canonically_ordered_add_monoid` instances for any finsupp with codomain a `canonically_ordered_add_monoid` & `has_ordered_sub`. * Provide `has_ordered_sub` instance in the same situation * Generalize lemmas about `nat` to this situation. * Prove some lemmas as special cases of `has_ordered_sub` lemmas. These will be removed in a subsequent PR. * Simplify some lemmas about `α →₀ ℕ` using `has_ordered_sub` lemmas. * Prove `nat.one_le_iff_ne_zero` (it's the second time I want to use it this week) Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>