theorem obvious_fact_1 (n : ℤ) (h : n ≥ 1) (x : ℤ) : x + n ≠ x

theorem helper_fact {a : ℤ} {b : ℤ} {n : ℤ} {x : ℤ} {y : ℤ} (h : a * x + b * y = n) : n = a * (x - b) + b * (y + a)

theorem helper_fact_2 {a : ℤ} {b : ℤ} {n : ℤ} {x : ℤ} {y : ℤ} (h : a ≥ 1 ∧ b ≥ 1 ∧ a * x + b * y = n ∧ n > 2 * a * b - a - b) : x ≥ b ∨ y ≥ a

theorem Lemma_1_61 (a : ℤ) (b : ℤ) (n : ℤ) (x : ℤ) (y : ℤ) (h_sol_xy : a * x + b * y = n) (a_pos : a ≥ 1) (b_pos : b ≥ 1) (x_nneg : x ≥ 0) (y_nneg : y ≥ 0) (n_geq : n > 2 * a * b - a - b) : ∃ (x1 : ℤ) (y1 : ℤ), x1 ≥ 0 ∧ y1 ≥ 0 ∧ a * x1 + b * y1 = n ∧ (x1 ≠ x ∨ y1 ≠ y)