English
An auxiliary function gcdAux implements the Euclidean algorithm to compute gcd(a,b) by iterating with the pair (a,b) replaced by (b mod a, a).
Русский
Вспомогательная функция gcdAux реализует Евклидово алгоритм вычисления НОД, повторяя замену пары (a,b) на (b mod a, a).
LaTeX
$$$\\gcdAux : \\mathbb{N} \\to \\operatorname{Num} \\to \\operatorname{Num} \\to \\operatorname{Num},\\; \\gcdAux(0,\\_,b) = b,\\; \\gcdAux(\\operatorname{succ}\\_,0,b) = b,\\; \\gcdAux(\\operatorname{succ} n, a, b) = \\gcdAux(n, (b \\bmod a), a).$$$
Lean4
/-- Auxiliary definition for `Num.gcd`. -/
def gcdAux : Nat → Num → Num → Num
| 0, _, b => b
| Nat.succ _, 0, b => b
| Nat.succ n, a, b => gcdAux n (b % a) a
