Theorem: oddpow_neg (ECTate/Algebra/Ring/Basic.lean)

State before:
R : Type u_1
inst✝ : CommRing R
n m : ℕ
a : R
h : n = 2 * m + 1
⊢ (-a) ^ n = -a ^ n
Tactic:
rw [h, pow_succ, evenpow_neg a (show 2 * m = 2 * m by rfl), ←neg_mul_eq_neg_mul, ←pow_succ,
  Nat.add_one]
State after:
no goals

State before:
R : Type u_1
inst✝ : CommRing R
n m : ℕ
a : R
h : n = 2 * m + 1
⊢ 2 * m = 2 * m
Tactic:
rfl
State after:
no goals