1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11

import Mathlib

-- https://lean-lang.org/doc/reference/latest//The--grind--tactic/#grind

example (n : ℕ) (h : n > 5) : ∃ a b, 3 * a + 4 * b = n := by
  use (n - (n % 3) * 4) / 3, n % 3
  grind

example (n x y : ℕ) (h : n > x * y - x - y) (hp : gcd x y = 1) : ∃ a b, a * x + b * y = n := by
  use (n - (n % x) * y) / x, n % x
  grind