let k, n, l be Nat; :: thesis: ( l >= 1 & n >= k * l implies n >= k )
assume that
A1: l >= 1 and
A2: n >= k * l ; :: thesis: n >= k
k * l >= k by A1, Th33;
hence n >= k by A2, XXREAL_0:2; :: thesis: verum