no goals
α : Type u_1
β : Type ?u.18224
ι : Type ?u.18227
π : ι → Type ?u.18232
inst✝ : IdemSemiring α
a✝ b c : α
n : ℕ
x✝ : n + 2 ≠ 0
a : α
⊢ (n + 2) • a = a
rw [succ_nsmul, nsmul_eq_self n.succ_ne_zero, add_idem]