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