theorem congr_args {x₀ y₀ a b x y : ℤ} : (x, y) = (x₀, y₀) → a * x + b * y = a * x₀ + b * y₀

theorem lemma_1_64 (x₀ y₀ a b x y : ℤ) (h1 : a > 0) (h2 : b > 0) (h5 : IsCoprime a b) (h6 : x₀ < b) (h7 : y₀ < a) (h8 : x ≥ 0) (h9 : y ≥ 0) : a * x + b * y = a * x₀ + b * y₀ ↔ (x, y) = (x₀, y₀)