English
xgcdAux is the recursive step used in the extended gcd algorithm: if r ≠ 0, set q = r' / r and recurse with updated values.
Русский
xgcdAux — рекурсивный шаг расширенного алгоритма Евклида: если r ≠ 0, пусть q = r'/r и продолжим с обновленными значениями.
LaTeX
$$$$ xgcdAux(r,s,t,r',s',t') = \\begin{cases} (r',s',t'), & r=0 \\\\ xgcdAux(r' \\, \\%\\, r,\\; s' - (r'/r) \\cdot s,\\; t' - (r'/r) \\cdot t,\\; r, s, t), & r \\neq 0 \\end{cases} $$$$
Lean4
@[elab_as_elim]
theorem induction {P : R → R → Prop} (a b : R) (H0 : ∀ x, P 0 x) (H1 : ∀ a b, a ≠ 0 → P (b % a) a → P a b) : P a b := by
classical
exact
if a0 : a = 0 then a0.symm ▸ H0 b
else
have _ := mod_lt b a0
H1 _ _ a0 (GCD.induction (b % a) a H0 H1)
termination_by a
