α : Type ?u.858461
p : PosNum
⊢ toZNumNeg (pos p) = ZNum.neg p
α : Type ?u.858461
p : PosNum
⊢ toZNumNeg (PosNum.pred' (succ' (pos p))) = ZNum.neg p
rw [PosNum.pred'_succ']
no goals
α : Type ?u.858461
p : PosNum
⊢ toZNumNeg (pos p) = ZNum.neg p
rfl
no goals
α : Type ?u.858461
p : PosNum
⊢ ZNum.succ (ZNum.pred (ZNum.pos p)) = ZNum.pos p
rw [ZNum.pred, ← toZNum_succ, Num.succ, PosNum.succ'_pred', toZNum]