feat(algebra/group_power/basic): `pow_add_pow_le` (#6037)
feat(algebra/group_power/basic): `pow_add_pow_le` (#6037)

For natural `n ≠ 0` and nonnegative `x, y` in an `ordered_semiring`, `x ^ n + y ^ n ≤ (x + y) ^ n`.





leanprover-community/mathlib,leanprover-community/mathlib