α : Type ?u.676222
a : PosNum
⊢ Num.toZNumNeg (pred' (PosNum.bit0 a)) = ZNum.bit1 (neg a)
α : Type ?u.676222
a : PosNum
⊢ sub' 1 (_root_.bit0 a) = ZNum.bit1 (neg a)
rw [PosNum.one_sub', a.bit0_of_bit0]
no goals
α : Type ?u.676222
a : PosNum
⊢ Num.toZNumNeg (pred' (PosNum.bit0 a)) = ZNum.bit1 (neg a)
rfl