theorem Th8: :: LIOUVIL1:5

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