for k, n being Nat holds (n !) / (k !) > 0 by XREAL_1:139;