mathlib

5ac586a6 - feat(algebra/group_power/order): When a power is less than one (#9700)

feat(algebra/group_power/order): When a power is less than one (#9700) This proves a bunch of simple order lemmas relating `1`, `a` and `a ^ n`. I also move `pow_le_one` upstream as it could already be proved in `algebra.group_power.order` and remove `[nontrivial R]` from `one_lt_pow`.