theorem ES: :: NEWTON04:70

for k, n being Nat holds (n !) * (k !) <= (n + k) !