Bezout's identity

import Mathlib

theorem bezout (a b : ℤ) (h : a ≠ 0 ∨ b ≠ 0) : ∃ x y : ℤ, a * x + b * y = Int.gcd a b := by
  have _ := h
  use Int.gcdA a b, Int.gcdB a b
  exact (Int.gcd_eq_gcd_ab a b).symm