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

( 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