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
consider t being Nat such that
A3: n = (k * (n div k)) + t and
A4: t < k by A1, NAT_D:def 1;
thus n < k by A2, A3, A4; :: thesis: verum