apply dvd_add
case mp
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a * x + b * y
case mp.h₁
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a * x

case mp.h₂
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ b * y