let k, n be Nat; :: thesis: ( k >= 1 implies n <= k * n )
assume k >= 1 ; :: thesis: n <= k * n
then 1 * n <= k * n by NAT_1:4;
hence n <= k * n ; :: thesis: verum