1 主定理

最大公約数が存在する：\(a, b\) の公約数 \(g\) で、どの公約数でも割り切れるものがある。
\(a + b\) についての強い帰納法で、互除法の手順をそのままなぞります。\(b = 0\) なら \(a\)。\(a = c + b\) なら \((c, b)\) と公約数が同じ（0.book の ∣+・∣sub）。\(a < b\) なら入れ替えます。
\(a , b \in \mathbb{M} \Longrightarrow \exists g \in \mathbb{M} . g \mid a , g \mid b , \forall d \in \mathbb{M} . ( d \mid a , d \mid b \Longrightarrow d \mid g )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄 ，1.