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