no goals
α : Type ?u.959671
n : ℕ
⊢ ofInt' ↑(n + 1) = -ofInt' -[n+1]
simp only [ofInt', Num.zneg_toZNumNeg]
α : Type ?u.959671
⊢ Num.toZNum 0 = -Num.toZNum 0
α : Type ?u.959671
⊢ Num.toZNum (Num.ofNat' 0) = -Num.toZNum (Num.ofNat' 0)
rw [Num.ofNat'_zero]
no goals
α : Type ?u.959671
⊢ Num.toZNum 0 = -Num.toZNum 0
rfl
no goals
α : Type ?u.959671
n : ℕ
⊢ Num.toZNumNeg (Num.ofNat' (Nat.add n 0 + 1)) = -Num.toZNum (Num.ofNat' (n + 1))
rw [Num.zneg_toZNum]