α : Type ?u.1057236
n : ℕ
⊢ Num.toZNumNeg ↑(n + 1) = -↑(n + 1)
α : Type ?u.1057236
n : ℕ
⊢ ofInt' -[n+1] = ↑-[n+1]
show Num.toZNumNeg (n + 1 : ℕ) = -(n + 1 : ℕ)
α : Type ?u.1057236
n : ℕ
⊢ succ (Num.toZNum ↑n) = succ ↑n
α : Type ?u.1057236
n : ℕ
⊢ Num.toZNumNeg ↑(n + 1) = -↑(n + 1)
rw [← neg_inj, neg_neg, Nat.cast_succ, Num.add_one, Num.zneg_toZNumNeg, Num.toZNum_succ,
  Nat.cast_succ, ZNum.add_one]
no goals
α : Type ?u.1057236
n : ℕ
⊢ succ (Num.toZNum ↑n) = succ ↑n
rfl