no goals
α : Type ?u.254897
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonAssocSemiring R
a : R
n : ℕ
⊢ n • a = a * ↑n
induction' n with n ih <;> [rw [zero_nsmul, Nat.cast_zero, mul_zero];
  rw [succ_nsmul', ih, Nat.cast_succ, mul_add, mul_one]]