mathlib3

dd4c2044 - feat(algebra/group_power/order): add monotonicity lemmas (#17895)

feat(algebra/group_power/order): add monotonicity lemmas (#17895) The existing `strict_mono_pow` lemma is renamed to `pow_strict_mono_right` to match the new `pow_strict_mono_right'`. From [this zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/If.20.60a.20.2B.20b.20.E2.89.A4.202.20*.20c.60.20then.20one.20of.20them.20is.20.60.E2.89.A4.20.20c.60/near/315126357). Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>