chore(algebra/group_power/lemmas): Lemmas about gsmul (#8618)
chore(algebra/group_power/lemmas): Lemmas about gsmul (#8618)

This restates some existing lemmas as `monotone` and `strict_monotone`, and provides new lemmas about the right argument of gsmul:

* `gsmul_le_gsmul'`
* `gsmul_lt_gsmul'`
* `gsmul_le_gsmul_iff'`
* `gsmul_lt_gsmul_iff'`

This also removes an unnecessary `linear_order` assumption from `gsmul_le_gsmul_iff` and `gsmul_lt_gsmul_iff`.



Co-authored-by: Eric Wieser <da64e90baec5d084ce3d8e05f3b022ae6d118ff5@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib