mathlib

bfd28571 - feat(algebra/order/ring): generalize some `mono` lemmas, use them (#14691)

feat(algebra/order/ring): generalize some `mono` lemmas, use them (#14691) * generalize lemmas like `monotone_mul_left_of_nonneg` to `ordered_semiring`s, add `decidable.*` versions as needed; * add some `antitone` lemmas; * use these lemmas to prove `le_of_mul_le_mul_left` etc; * use section-local attributes instead of `letI := @linear_order.decidable_le α _`.