let a, b be Nat; :: thesis: ( b <> 0 implies ex k being Element of NAT st
( k * b <= a & a < (k + 1) * b ) )
set k9 = a div b;
assume b <> 0 ; :: thesis: ex k being Element of NAT st
( k * b <= a & a < (k + 1) * b )
then A1: ex t being Nat st
( a = (b * (a div b)) + t & t < b ) by NAT_D:def 1;
((a div b) + 1) * b = ((a div b) * b) + b ;
then ((a div b) + 1) * b > a by A1, XREAL_1:6;
hence ex k being Element of NAT st
( k * b <= a & a < (k + 1) * b ) by A1, NAT_1:11; :: thesis: verum