Constant descent Vieta jumping.

This proof technique allows one to prove an arbitrary proposition claim, by running a descent argument on a hyperbola H in the first quadrant of the plane, under the following conditions:

• h₀ : There exists an integral point (x,y) on the hyperbola H.
• H_symm : The hyperbola has a symmetry along the diagonal in the plane.
• H_zero : If an integral point (x,0) lies on the hyperbola H, then claim is true.
• H_diag : If an integral point (x,x) lies on the hyperbola H, then claim is true.
• H_desc : If (x,y) is an integral point on the hyperbola H, with x < y then there exists a “smaller” point on H: a point (x',y') with x' < y' ≤ x.

For reasons of usability, the hyperbola H is implemented as an arbitrary predicate. (In question 6 of IMO1988, where this proof technique was first developped, the predicate claim would be ∃ (d : ℕ), d ^ 2 = k for some natural number k, and the predicate H would be λ a b, a * a + b * b = (a * b + 1) * k.)

To ensure that the predicate H actually describes a hyperbola, the user must provide arguments B and C that are used as coefficients for a quadratic equation. Finally, H_quad is the proof obligation that the quadratic equation (y:ℤ) * y - B x * y + C x = 0 describes the same hyperbola as the predicate H.

For extra flexibility, one must provide a predicate base on the integral points in the plane. In the descent step H_desc this will give the user the additional assumption that the point (x,y) does not lie in this base locus. The user must provide a proof that the proposition claim is true if there exists an integral point (x,y) on the hyperbola H that lies in the base locus. If such a base locus is not necessary, once can simply let it be λ x y, false.

Question 6 of IMO1988. If a and b are two natural numbers such that a*b+1 divides a^2 + b^2, show that their quotient is a perfect square.