α : Type ?u.961215
⊢ Num.toZNum (Num.ofNat' 0) = 0
α : Type ?u.961215
⊢ ofInt' ↑0 = 0
dsimp [ofInt', cast_zero]
no goals
α : Type ?u.961215
⊢ Num.toZNum (Num.ofNat' 0) = 0
erw [Num.ofNat'_zero, Num.toZNum]
α : Type ?u.961215
a : PosNum
⊢ Num.toZNum (Num.pos a) = pos a
α : Type ?u.961215
a : PosNum
⊢ ofInt' ↑(pos a) = pos a
rw [cast_pos, ← PosNum.cast_to_nat, ← Num.ofInt'_toZNum, PosNum.of_to_nat]
no goals
α : Type ?u.961215
a : PosNum
⊢ Num.toZNum (Num.pos a) = pos a
rfl
α : Type ?u.961215
a : PosNum
⊢ -Num.toZNum (Num.pos a) = neg a
α : Type ?u.961215
a : PosNum
⊢ ofInt' ↑(neg a) = neg a
rw [cast_neg, ofInt'_neg, ← PosNum.cast_to_nat, ← Num.ofInt'_toZNum, PosNum.of_to_nat]
no goals
α : Type ?u.961215
a : PosNum
⊢ -Num.toZNum (Num.pos a) = neg a
rfl