A bound for integer roots of monic quadratics

An integer satisfying y² + by = c has absolute value at most |b| + |c| + 1. This bound makes searches for integer solutions of equations quadratic in one coordinate finite.

theorem TauCeti.abs_le_of_quadratic_eq {y b c : ℤ} (h : y ^ 2 + b * y = c) : |y| ≤ |b| + |c| + 1

An integer root of Y² + bY = c is bounded by the absolute values of its coefficients.