Documentation

Acmoi.Exercise1_5

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
instance example_1_59 :
Decidable (∀ (x y : ), 2 * x + 3 * y = 7 (x > 0y > 0) x = 2 y = 1)
Equations