let x, y be Element of INT ; :: thesis: ( abs y <> 0 implies abs (x mod y) < abs y )
assume A1: abs y <> 0 ; :: thesis: abs (x mod y) < abs y

per cases ( 0 < y or y <= 0 ) ;

suppose C1: 0 < y ; :: thesis: abs (x mod y) < abs y

then C2: x mod y < y by INT_1:58;
0 <= x mod y by INT_1:57, C1;
then C3: abs (x mod y) < y by ABSVALUE:def 1, C2;
y <= abs y by ABSVALUE:4;
hence abs (x mod y) < abs y by C3, XXREAL_0:2; :: thesis: verum

end;

suppose C4: y <= 0 ; :: thesis: abs (x mod y) < abs y

C40P: y <> 0 by ABSVALUE:2, A1;
C41: - (x mod y) < - y by INT158A, C40P, C4;
XX1: x mod y <= 0 by C4, INT157A;
C42: abs (x mod y) = - (x mod y)

proof

per cases ( x mod y = 0 or x mod y <> 0 ) ;

suppose x mod y = 0 ; :: thesis: abs (x mod y) = - (x mod y)

hence abs (x mod y) = - (x mod y) by ABSVALUE:2; :: thesis: verum

end;

suppose x mod y <> 0 ; :: thesis: abs (x mod y) = - (x mod y)

hence abs (x mod y) = - (x mod y) by ABSVALUE:def 1, XX1; :: thesis: verum

end;

end;

end;

thus abs (x mod y) < abs y by C42, C41, C40P, C4, ABSVALUE:def 1; :: thesis: verum

end;

end;