for n1, n being Nat st n <= n1 holds
n ! <= n1 ! by Lm51;