for n, i being Nat st n >= 2 & i >= 1 holds
(n + i) ! > (n !) + i