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