[GOAL]
G : Type u_1
inst✝ : Group G
a b : G
n m : ℤ
⊢ a * b ^ n * b ^ m = a * b ^ (n + m)
[PROOFSTEP]
rw [mul_assoc, ← zpow_add]
[GOAL]
G : Type u_1
inst✝ : Group G
a b : G
m : ℤ
⊢ a * b * b ^ m = a * b ^ (m + 1)
[PROOFSTEP]
rw [mul_assoc, mul_self_zpow]
[GOAL]
G : Type u_1
inst✝ : Group G
a b : G
n : ℤ
⊢ a * b ^ n * b = a * b ^ (n + 1)
[PROOFSTEP]
rw [mul_assoc, mul_zpow_self]
