theorem lem10: :: LAGRA4SQ:11

for x1, h being Nat
for y1 being Integer st 1 < h & x1 mod h = y1 mod h & y1 = 0 holds
ex m1 being Integer st x1 = h * m1