theorem :: IRRAT_1:33

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