We first prove, informally but constructively, that Z is a ring without zero-divisors. Then, using Per Martin-Löf's type theory, we establish the same result formally. This is done following the informal reasoning closely. The proofs are automatically checked by using the proof-checker ``TWB'' developed by us at SICS. In the proofs we use only the basic set-theoretic axioms in type theory.