let b be Integer; :: thesis: ( b > 0 implies for a being Integer ex q, r being Integer st
( a = (b * q) + r & r >= 0 & r < b ) )
assume A1: b > 0 ; :: thesis: for a being Integer ex q, r being Integer st
( a = (b * q) + r & r >= 0 & r < b )
let a be Integer; :: thesis: ex q, r being Integer st
( a = (b * q) + r & r >= 0 & r < b )

per cases ( a >= 0 or a < 0 ) ;

suppose a >= 0 ; :: thesis: ex q, r being Integer st
( a = (b * q) + r & r >= 0 & r < b )

then a in NAT by INT_1:16;
then A2: a is Nat ;
b in NAT by A1, INT_1:16;
then b is Nat ;
then consider k, t being Nat such that
A3: ( a = (b * k) + t & t < b ) by A1, A2, NAT_1:17;
take q = k; :: thesis: ex r being Integer st
( a = (b * q) + r & r >= 0 & r < b )
take r = t; :: thesis: ( a = (b * q) + r & r >= 0 & r < b )
thus ( a = (b * q) + r & r >= 0 & r < b ) by A3; :: thesis: verum

end;

suppose a < 0 ; :: thesis: ex q, r being Integer st
( a = (b * q) + r & r >= 0 & r < b )

then a <= - 0 ;
then - a >= 0 ;
then - a in NAT by INT_1:16;
then A4: - a is Nat ;
b in NAT by A1, INT_1:16;
then b is Nat ;
then consider k, t being Nat such that
A5: ( - a = (b * k) + t & t < b ) by A1, A4, NAT_1:17;

per cases ( t = 0 or t <> 0 ) ;

suppose t = 0 ; :: thesis: ex q, r being Integer st
( a = (b * q) + r & r >= 0 & r < b )

then A6: a = b * (- k) by A5;
take q = - k; :: thesis: ex r being Integer st
( a = (b * q) + r & r >= 0 & r < b )
take r = 0 ; :: thesis: ( a = (b * q) + r & r >= 0 & r < b )
thus a = (b * q) + r by A6; :: thesis: ( r >= 0 & r < b )
thus ( r >= 0 & r < b ) by A1; :: thesis: verum

end;

suppose t <> 0 ; :: thesis: ex q, r being Integer st
( a = (b * q) + r & r >= 0 & r < b )

then A7: t > 0 ;
A8: a = (b * ((- k) - 1)) + (b - t) by A5;
take q = (- k) - 1; :: thesis: ex r being Integer st
( a = (b * q) + r & r >= 0 & r < b )
take r = b - t; :: thesis: ( a = (b * q) + r & r >= 0 & r < b )
thus a = (b * q) + r by A8; :: thesis: ( r >= 0 & r < b )
thus ( r >= 0 & r < b ) by A5, A7, XREAL_1:46, XREAL_1:52; :: thesis: verum

end;

end;

end;

end;