theorem decide_diophantine2_1 {a b n x y : ℕ} (h : a * x + b * y = n) (ha : 0 < a) : x < n / a + 1

theorem decide_diophantine2_2 {a b n x y : ℕ} (g1 : a * x + b * y = n) (ha : 0 < a) (hb : 0 < b) : x < n / a + 1 ∧ y < n / b + 1

@[implicit_reducible]

instance example_1_59 : Decidable (∀ (x y : ℕ), 2 * x + 3 * y = 7 ∧ (x > 0 → y > 0) ↔ x = 2 ∧ y = 1)

Equations

• example_1_59 = decidable_of_iff (∀ (x : Fin (7 / 2 + 1)) (y : Fin (7 / 3 + 1)), 2 * ↑x + 3 * ↑y = 7 ∧ (↑x > 0 → ↑y > 0) ↔ ↑x = 2 ∧ ↑y = 1) example_1_59._proof_1