1 互除法の漸化式

\(a \gcd b\) を、互除法の漸化式（gcd𝕄・articles3/69 と同じ）を満たす関数として仮定します。それが最大公約数であることは 69 で示しました（69 は自然数を公理で与えた本なので、ここでは import せず仮定だけを書きます）。
word(ss,s) … \(\gcd\)
gcd𝕄 … \(\begin{cases} a \in \mathbb{M} \Longrightarrow a \gcd 0 = a \\ a , b \in \mathbb{M} \Longrightarrow a \gcd b = b \gcd a \\ a , b \in \mathbb{M} \Longrightarrow ( a + b ) \gcd b = a \gcd b \end{cases}\)

2 主定理

自然数 \(a, b\) に対して、\(as + bt = a \gcd b\) となる整数 \(s, t\) がある（Bézout）。
\(a + b\) についての強い帰納法で示します。\(b = 0\) なら \(s = 1, t = 0\)。\(a = c + b\) で \(cs + bt = c \gcd b\) なら \(as + b(t - s) = a \gcd b\)。\(a < b\) なら入れ替えます。
\(a , b \in \mathbb{M} \Longrightarrow \exists s \in \mathbb{Z} . \exists t \in \mathbb{Z} . a \cdot s + b \cdot t = a \gcd b\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，+𝕄 ，*𝕄 ，-ℤ ，+ℤ ，*ℤ ，gcd𝕄