let k, n be Nat; :: thesis: ( k > 0 & n div k = 0 implies n < k )
assume that
A1: k > 0 and
A2: n div k = 0 ; :: thesis: n < k
ex t being Nat st
( n = (k * (n div k)) + t & t < k ) by A1, NAT_D:def 1;
hence n < k by A2; :: thesis: verum