mathlib3

faba9cea - chore(algebra/group_power): generalize `semiring` version of Bernoulli's inequality (#5831)

chore(algebra/group_power): generalize `semiring` version of Bernoulli's inequality (#5831) Now `one_add_mul_le_pow'` assumes `0 ≤ a * a`, `0 ≤ (1 + a) * (1 + a)`, and `0 ≤ 2 + a`. Also add a couple of convenience lemmas.