Yes, but in a software like a theorem prover you must make the conscious decision whether you want your prover to be able to assume ℕ ⊂ ℤ or not. All the type theory based ones say "not". That is not very convenient.