Commit 2022-08-22 06:09 bfd28571

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

• generalize lemmas like monotone_mul_left_of_nonneg to ordered_semirings, 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 α _.