no goals
R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑(-↑0) = -↑↑0
erw [cast_zero, neg_zero]
no goals
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(-↑(n + 1)) = -↑↑(n + 1)
erw [cast_ofNat, cast_negSucc]
no goals
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(- -[n+1]) = -↑-[n+1]
erw [cast_ofNat, cast_negSucc, neg_neg]