English
A helper function for the extended GCD algorithm, producing the data required for the extended gcd process.
Русский
Помогательная функция для алгоритма расширенного НОД, возвращающая данные, необходимые для расширенного НОД.
LaTeX
$$$xgcdAux : \mathbb{N} \to \mathbb{Z} \to \mathbb{Z} \to \mathbb{N} \to \mathbb{Z} \to \mathbb{Z} \to \mathbb{N} \times \mathbb{Z} \times \mathbb{Z}$$$
Lean4
/-- Helper function for the extended GCD algorithm (`Nat.xgcd`). -/
def xgcdAux : ℕ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ
| 0, _, _, r', s', t' => (r', s', t')
| succ k, s, t, r', s', t' =>
let q := r' / succ k
xgcdAux (r' % succ k) (s' - q * s) (t' - q * t) (succ k) s t
termination_by k => k
decreasing_by exact mod_lt _ <| (succ_pos _).gt
