chore(algebra/group_power): golf a few proofs (#10498)
* move `pow_lt_pow_of_lt_one` and `pow_lt_pow_iff_of_lt_one` from
`algebra.group_power.lemmas` to `algebra.group_power.order`;
* add `strict_anti_pow`, use it to golf the proofs of the two lemmas
above;
* golf a few other proofs;
* add `nnreal.exists_pow_lt_of_lt_one`.
