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