English
In a Euclidean domain, there is an induction principle for gcd: for any P(a,b), if P holds when a=0, and P(a,b) holds when a ≠ 0 and P(b mod a, a) assuming P(a,b) for smaller gcd, then P(a,b) holds for all a,b.
Русский
В евклидовом кольце существует принцип индукции по НОД: для любых a,b (свойство P) выполняется, если P(0,b) и P(b mod a, a) при условии меньшего НОД выполняются, тогда P(a,b) выполняется для всех a,b.
LaTeX
$$$$ \\text{ГДП индукция: } \\forall a,b,\\; (\\forall x\\; P(0,x)) \\land (\\forall a,b\\, (a\\neq 0) \\Rightarrow P(x) \\Rightarrow P(a,b)) \\Rightarrow P(a,b). $$$$
Lean4
/-- An implementation of the extended GCD algorithm.
At each step we are computing a triple `(r, s, t)`, where `r` is the next value of the GCD
algorithm, to compute the greatest common divisor of the input (say `x` and `y`), and `s` and `t`
are the coefficients in front of `x` and `y` to obtain `r` (i.e. `r = s * x + t * y`).
The function `xgcdAux` takes in two triples, and from these recursively computes the next triple:
```
xgcdAux (r, s, t) (r', s', t') = xgcdAux (r' % r, s' - (r' / r) * s, t' - (r' / r) * t) (r, s, t)
```
-/
def xgcdAux (r s t r' s' t' : R) : R × R × R :=
if _hr : r = 0 then (r', s', t')
else
let q := r' / r
have _ := mod_lt r' _hr
xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t
termination_by r
