????在自然數(shù)的部分中，我們定義的自然數(shù)的減法滿足：當(dāng) a < b 時(shí)，a - b = 0。這使得自然數(shù)的減法的性質(zhì)具有局限性，經(jīng)常需要分類討論。為了得到性質(zhì)更完整、更合理的減法，我們需要引入整數(shù)。

????現(xiàn)在，我們假設(shè)已經(jīng)聲明了整數(shù)類型 Z 和輸出整數(shù)的自然數(shù)的減法 "-" : nat -> nat -> Z。我們希望任何整數(shù)都可以表示成兩個(gè)自然數(shù)相減的形式。除此之外，還需要讓 a "-" b = c "-" d 當(dāng)且僅當(dāng) a + d = b + c?；谶@些需求，我們可以像構(gòu)造基數(shù)一樣，通過(guò)等價(jià)類構(gòu)造整數(shù)。

????我們首先定義 nat * nat 上的等價(jià)關(guān)系 Zeq，從這個(gè)等價(jià)關(guān)系出發(fā)即可構(gòu)造出類型 Z。對(duì)于自然數(shù) a 和 b，Z_make (a,b) 是整數(shù)。Z_make 相當(dāng)于之前假設(shè)中的 "-"。對(duì)于整數(shù) x，Z構(gòu)造NN x 是兩個(gè)自然數(shù)組成的有序?qū)?，滿足?Z_make?(Z構(gòu)造NN x)?=?x。

????對(duì)于自然數(shù) n，Z_make (n,0) 可以被視為 n?自然對(duì)應(yīng)的整數(shù)，這里記作 n.z。

????對(duì)于整數(shù)的加法，我們希望?Z_make (a,b) + Z_make (c,d) = Z_make (a+c,b+d)。具體定義與性質(zhì)如下：

????對(duì)于整數(shù) x，我們可以定義它的相反數(shù) - x。我們希望 - Z_make (a,b) = Z_make (b,a)。具體定義與性質(zhì)如下：

????現(xiàn)在我們可以定義整數(shù)的減法。對(duì)于整數(shù) x 和 y，我們定義 x - y = x + (- y) 。這與 Z_make 一致。

????在以上定理中我們可以看出，整數(shù)的加減法能夠能夠完美地交融在一起，這是自然數(shù)的加減法所不具備的。

????我們還可以定義整數(shù)的乘法，這比整數(shù)的加法更復(fù)雜。

????對(duì)于整數(shù) x，x 是正數(shù)當(dāng)且僅當(dāng) x 是某個(gè)非零自然數(shù)自然對(duì)應(yīng)的整數(shù)；x 是負(fù)數(shù)當(dāng)且僅當(dāng) x 是某個(gè)非零自然數(shù)自然對(duì)應(yīng)的整數(shù)的相反數(shù)?？梢宰C明：一個(gè)整數(shù)要么是正數(shù)，要么是負(fù)數(shù)，要么是 0.z。

????利用以上性質(zhì)可以證明：