English
For natural numbers x,y, gcd(x,y) equals x·a + y·b for integers a,b given by the extended Euclidean algorithm.
Русский
Для целых x,y существует представление нац gcd(x,y) = x·a + y·b, где a,b получены алгоритмом расширенного Евклида.
LaTeX
$$$\gcd(x,y) = x\cdot gcdA(x,y) + y\cdot gcdB(x,y)\quad \text{in } \mathbb{Z}$$$
Lean4
/-- **Bézout's lemma**: given `x y : ℕ`, `gcd x y = x * a + y * b`, where `a = gcd_a x y` and
`b = gcd_b x y` are computed by the extended Euclidean algorithm.
-/
theorem gcd_eq_gcd_ab : (gcd x y : ℤ) = x * gcdA x y + y * gcdB x y :=
by
have := @xgcdAux_P x y x y 1 0 0 1 (by simp [P]) (by simp [P])
rwa [xgcdAux_val, xgcd_val] at this
