English
If gcd(p,q) divides n and n ≥ (p-1)(q-1), then there exist a,b ∈ ℕ with a p + b q = n.
Русский
Если gcd(p,q) делит n и n ≥ (p-1)(q-1), то найдутся a,b ∈ ℕ такие что a p + b q = n.
LaTeX
$$∃ a,b ∈ ℕ, a p + b q = n$$
Lean4
/-- If the gcd of two natural numbers `p` and `q` divides a third natural number `n`,
and if `n` is at least `(p - 1) * (q - 1)`, then `n` can be represented as an `ℕ`-linear
combination of `p` and `q`.
TODO: show that if `p.gcd q = 1` and `0 ≤ n ≤ (p - 1) * (q - 1) - 1 = N`, then `n` is
representable iff `N - n` is not. In particular `N` is not representable, solving the
coin problem for two coins: https://en.wikipedia.org/wiki/Coin_problem#n_=_2. -/
theorem exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le (p q n : ℕ) (dvd : p.gcd q ∣ n) (le : p.pred * q.pred ≤ n) :
∃ a b : ℕ, a * p + b * q = n := by
obtain _ | p := p
· have ⟨b, eq⟩ := q.gcd_zero_left ▸ dvd
exact ⟨0, b, by simpa [mul_comm, eq_comm] using eq⟩
obtain _ | q := q
· have ⟨a, eq⟩ := p.gcd_zero_right ▸ dvd
exact ⟨a, 0, by simpa [mul_comm, eq_comm] using eq⟩
rw [← Int.gcd_natCast_natCast, Int.gcd_dvd_iff] at dvd
have ⟨a_n, b_n, eq⟩ := dvd
let a := a_n % q.succ
let b := b_n + a_n / q.succ * p.succ
refine ⟨a.toNat, b.toNat, Nat.cast_injective (R := ℤ) ?_⟩
have : a * p.succ + b * q.succ = n := by
rw [add_mul, ← add_assoc, add_right_comm, mul_right_comm, ← add_mul, Int.emod_add_ediv_mul, eq, mul_comm,
mul_comm b_n]
rw [Nat.cast_add, Nat.cast_mul, Nat.cast_mul, Int.natCast_toNat_eq_self.mpr (Int.emod_nonneg _ <| by cutsat),
Int.natCast_toNat_eq_self.mpr, this]
-- show b ≥ 0 by contradiction
by_contra hb
replace hb : b ≤ -1 := by omega
apply lt_irrefl (n : ℤ)
have ha := Int.emod_lt a_n (by cutsat : (q.succ : ℤ) ≠ 0)
rw [p.pred_succ, q.pred_succ] at le
calc
n = a * p.succ + b * q.succ := this.symm
_ ≤ q * p.succ + -1 * q.succ := by gcongr <;> omega
_ = p * q - 1 := by simp_rw [Nat.cast_succ, mul_add, mul_comm]; cutsat
_ ≤ n - 1 := by rwa [sub_le_sub_iff_right, ← Nat.cast_mul, Nat.cast_le]
_ < n := by cutsat
