:: deftheorem Def1 defines div NAT_D:def 1 :
for k, l being natural Number
for b₃ being Nat holds
( b₃ = k div l iff ( ex t being Nat st
( k = (l * b₃) + t & t < l ) or ( b₃ = 0 & l = 0 ) ) );