for x1, h being Nat
for y1 being Integer st 1 < h & x1 mod h = y1 mod h & - h < 2 * y1 & (2 * y1) ^2 = h ^2 holds
( 2 * y1 = h & ex m1 being Nat st 2 * x1 = ((2 * m1) + 1) * h )