case neg
α : Type ?u.658662
a✝ : PosNum
⊢ -succ (neg a✝) = pred (-neg a✝)
α : Type ?u.658662
n : ZNum
⊢ -succ n = pred (-n)
cases n <;> try { rfl }
case neg
α : Type ?u.658662
a✝ : PosNum
⊢ Num.toZNum (pred' a✝) = pred (-neg a✝)
case neg
α : Type ?u.658662
a✝ : PosNum
⊢ -succ (neg a✝) = pred (-neg a✝)
rw [succ, Num.zneg_toZNumNeg]
no goals
case neg
α : Type ?u.658662
a✝ : PosNum
⊢ Num.toZNum (pred' a✝) = pred (-neg a✝)
rfl