实数的形式化 #2 自然数 (2) 自然数的其他运算

    这篇专栏将会讨论自然数的减法、带余除法、整除、最大公因数、最小公倍数、阶乘的定义与基本性质。

    以上代码定义了自然数的减法：a - b 定义为 a 取了 b 次前驱后得到的自然数。由于 0 的前驱是 0，因此当不够减时，返回的结果是 0。自然数的减法具有以下性质：

    自然数的减法还可以通过以下的算法定义：

    可以证明这两种减法运算是相等的，但是它们在语法结构上是不同的。新定义的 Nsub' 在一定条件下可以被 Coq 识别为子项，从而可以出现在 Fixpoint 中，例如下面的定义：（把 Nsub' 换为 Nsub 不符合 fix 表达式的限制条件，是语法错误）

    以上代码定义的 Ndiv_pre 描述的是这样一个过程：计算 Ndiv_pre a b q 时，不断地从 a 中减去 b.+1；a 每减去一次 b.+1，q 就加一；当 a 不够减时，以有序对的形式返回当前的 q 和 a。

    Ndiv_pre 为定义自然数的除法做了准备。自然数的除法的定义如下：

    a / b 是一个有序对 (商, 余数)，a // b 表示 a / b 的商，a % b 表示 a / b 的余数。规定 a / 0 = (0, a)。相关定理如下：

    a % b 的另一种算法：

    a 整除 b，当且仅当 b % a = 0。以下代码中用 a %| b 表示 a 整除 b，而我们通常直接写作 a | b。

    a 整除 b 等价于 exists c, b = a * c。自然数的整除关系是偏序关系，但不是全序关系。

    两个自然数的最大公因数（gcd）的定义如下：

    这个定义可能不太易于理解。从这个定义出发，我们可以先证明以下定理：

    “gcdE”定理反映了辗转相除法。基于此，我们可以证明以下定理：（部分定理的证明需要用到强归纳，核心思路在于通过 b <> 0 -> a % b < b 使用归纳假设）

    两个自然数的最小公倍数（lcm）的定义与基本性质如下：

    利用最大公因数，我们可以定义两个自然数的最简比：

    自然数的阶乘（a! = a*(a-1)*(a-2)*...*2*1）的定义如下：