nlinarith for 'sum of reciprocals is small' bounds: shift variables to x-X, y-Y, z-Z

Olympiad bounds such as 'K·xyz = xy+yz+zx+x+y+z with 1≤x<y<z forces K<3' (IMO 1992 P1) go through with one nlinarith call. The hints are hX : 0 ≤ x-X, hY : 0 ≤ y-Y, hZ : 0 ≤ z-Z (X, Y, Z the minimal values in the case) plus mul_nonneg hX hY, mul_nonneg hY hZ, mul_nonneg hX hZ, and mul_nonneg (mul_nonneg hX hY) hZ. The reason it works: after substituting x = x'+X etc., the polynomial K·xyz - (xy+…) has all coefficients positive, so a nonnegative combination of the hint products is the certificate. Without the triple product nlinarith times out or fails. Then interval_cases K and x, and finish (y-2)(z-2)=5 with a nlinarith bound on y followed by interval_cases y <;> omega.