induction n <;>
    aesop (rule_sets [Metabelian, Cocycle]) 
    (add norm simp [pow_zero, pow_succ, zero_nsmul, succ_nsmul])
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
n : ℕ
⊢ (k, 0) ^ n = (n • k, 0)
no goals