????這篇專欄將會(huì)討論自然數(shù)的減法、帶余除法、整除、最大公因數(shù)、最小公倍數(shù)、階乘的定義與基本性質(zhì)。

????以上代碼定義了自然數(shù)的減法：a - b 定義為 a 取了 b 次前驅(qū)后得到的自然數(shù)。由于 0 的前驅(qū)是 0，因此當(dāng)不夠減時(shí)，返回的結(jié)果是 0。自然數(shù)的減法具有以下性質(zhì)：

????自然數(shù)的減法還可以通過以下的算法定義：

????可以證明這兩種減法運(yùn)算是相等的，但是它們在語法結(jié)構(gòu)上是不同的。新定義的 Nsub' 在一定條件下可以被 Coq 識(shí)別為子項(xiàng)，從而可以出現(xiàn)在 Fixpoint 中，例如下面的定義：（把 Nsub' 換為 Nsub 不符合 fix 表達(dá)式的限制條件，是語法錯(cuò)誤）

????以上代碼定義的 Ndiv_pre?描述的是這樣一個(gè)過程：計(jì)算?Ndiv_pre a b q 時(shí)，不斷地從 a 中減去 b.+1；a 每減去一次 b.+1，q 就加一；當(dāng) a 不夠減時(shí)，以有序?qū)Φ男问椒祷禺?dāng)前的?q 和 a。

????Ndiv_pre 為定義自然數(shù)的除法做了準(zhǔn)備。自然數(shù)的除法的定義如下：

????a / b 是一個(gè)有序?qū)?(商, 余數(shù))，a // b 表示 a / b 的商，a % b 表示 a / b 的余數(shù)。規(guī)定 a / 0 = (0, a)。相關(guān)定理如下：

????a % b 的另一種算法：

????a 整除 b，當(dāng)且僅當(dāng) b % a = 0。以下代碼中用 a %| b 表示 a 整除 b，而我們通常直接寫作 a | b。

????a 整除?b 等價(jià)于?exists c, b = a * c。自然數(shù)的整除關(guān)系是偏序關(guān)系，但不是全序關(guān)系。

????兩個(gè)自然數(shù)的最大公因數(shù)（gcd）的定義如下：

????這個(gè)定義可能不太易于理解。從這個(gè)定義出發(fā)，我們可以先證明以下定理：

????“gcdE”定理反映了輾轉(zhuǎn)相除法。基于此，我們可以證明以下定理：（部分定理的證明需要用到強(qiáng)歸納，核心思路在于通過?b <> 0 -> a % b < b 使用歸納假設(shè)）

????兩個(gè)自然數(shù)的最小公倍數(shù)（lcm）的定義與基本性質(zhì)如下：

????利用最大公因數(shù)，我們可以定義兩個(gè)自然數(shù)的最簡比：

????自然數(shù)的階乘（a! = a*(a-1)*(a-2)*...*2*1）的定義如下：