no goals
R : Type u_1
S : Type ?u.109740
M : Type ?u.109743
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
a : R
n : ℕ
⊢ (-a) ^ bit1 n = -a ^ bit1 n
simp only [bit1, pow_succ, neg_pow_bit0, neg_mul_eq_neg_mul]