let n, k be Nat; :: thesis: ( 0 < n & n < k implies n ! < k ! )
assume A1: ( 0 < n & n < k ) ; :: thesis: n ! < k !
then n + 1 <= k by NAT_1:13;
then A2: (n + 1) ! <= k ! by SIN_COS:39;
n + 1 > 0 + 1 by A1, XREAL_1:6;
then ( (n + 1) ! = (n !) * (n + 1) & (n !) * (n + 1) > (n !) * 1 ) by NEWTON:15, XREAL_1:68;
hence n ! < k ! by A2, XXREAL_0:2; :: thesis: verum