let k, n be Nat; :: thesis: ( k > 0 & k <= n implies n div k >= 1 )
assume that
A1: k > 0 and
A2: k <= n ; :: thesis: n div k >= 1
n div k <> 0 by A1, A2, Th14;
then n div k > 0 ;
then n div k >= 0 + 1 by NAT_1:13;
hence n div k >= 1 ; :: thesis: verum