(n !) * (k !) <= (n + k) ! by ES;
then (n !) * (k !) < (n + k) ! by EZ, XXREAL_0:1;
then ((n !) * (k !)) - ((n !) * (k !)) < ((n + k) !) - ((n !) * (k !)) by XREAL_1:9;
then ((n + k) !) - ((n !) * (k !)) > 0 ;
hence ((n + k) !) - ((n !) * (k !)) is positive ; :: thesis: verum