no goals
F : Type ?u.74305
α✝ : Type ?u.74308
β : Type ?u.74311
γ : Type ?u.74314
inst✝¹ : Monoid α✝
s t : Set α✝
a : α✝
m n✝ : ℕ
α : Type u_1
inst✝ : AddMonoid α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (n + 2) • univ = univ
rw [succ_nsmul, nsmul_univ n.succ_ne_zero, univ_add_univ]