theorem :: WSIERP_1:38

for a being Nat
for k being Integer st a <> 0 & a gcd k = 1 holds
ex b, e being Nat st
( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )