no goals
R : Type u_1
S : Type ?u.92208
M : Type ?u.92211
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = -1
⊢ (-1) ^ (n + 1) = 1
rw [pow_succ, h, neg_one_mul, neg_neg]
no goals
R : Type u_1
S : Type ?u.92208
M : Type ?u.92211
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = 1
⊢ (-1) ^ (n + 1) = -1
rw [pow_succ, h, mul_one]