### Topic: gcd

Can we find somewhere in Isabelle a version of `lemma bezout_gcd_nat`

(in HOL/Computational_Algebra/Primes) but for integers?

You probably want this from `HOL-Computational_Algebra.Euclidean_Algorithm`

:

```
lemma bezout_coefficients:
assumes "bezout_coefficients a b = (x, y)"
shows "x * a + y * b = gcd a b"
```

Works for any Euclidean ring.

Last updated: Oct 13 2024 at 01:36 UTC