feat: a * a ^ (n - 1) = a ^ n (#9610)

From LeanAPAP

Author: YaelDillies

Mathlib/Algebra/Group/Commute/Defs.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Neil Strickland, Yury Kudryashov
 -/
 import Mathlib.Algebra.Group.Semiconj.Defs
+import Mathlib.Data.Nat.Defs
 
 #align_import algebra.group.commute from "leanprover-community/mathlib"@"05101c3df9d9cfe9430edc205860c79b6d660102"
 
@@ -209,12 +210,6 @@ theorem pow_pow_self (a : M) (m n : ℕ) : Commute (a ^ m) (a ^ n) :=
 #align add_commute.nsmul_nsmul_self AddCommute.nsmul_nsmul_selfₓ
 -- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`
 
-@[to_additive succ_nsmul']
-theorem _root_.pow_succ' (a : M) (n : ℕ) : a ^ (n + 1) = a ^ n * a :=
-  (pow_succ a n).trans (self_pow _ _)
-#align pow_succ' pow_succ'
-#align succ_nsmul' succ_nsmul'
-
 end Monoid
 
 section DivisionMonoid
@@ -253,6 +248,25 @@ end Group
 
 end Commute
 
+section Monoid
+variable {M : Type*} [Monoid M] {n : ℕ}
+
+@[to_additive succ_nsmul']
+lemma pow_succ' (a : M) (n : ℕ) : a ^ (n + 1) = a ^ n * a :=
+  (pow_succ a n).trans (Commute.self_pow _ _)
+#align pow_succ' pow_succ'
+#align succ_nsmul' succ_nsmul'
+
+@[to_additive]
+lemma mul_pow_sub_one (hn : n ≠ 0) (a : M) : a * a ^ (n - 1) = a ^ n := by
+  rw [← pow_succ, Nat.sub_add_cancel $ Nat.one_le_iff_ne_zero.2 hn]
+
+@[to_additive]
+lemma pow_sub_one_mul (hn : n ≠ 0) (a : M) : a ^ (n - 1) * a = a ^ n := by
+  rw [← pow_succ', Nat.sub_add_cancel $ Nat.one_le_iff_ne_zero.2 hn]
+
+end Monoid
+
 section CommGroup
 
 variable [CommGroup G] (a b : G)