let n, k be Nat; :: thesis: (min (n,k)) ! divides n !
reconsider m = min (n,k) as Nat ;
n - m >= m - m by XREAL_1:9, XXREAL_0:17;
then reconsider d = n - m as Nat ;
m ! divides (m + d) ! by MDF;
hence (min (n,k)) ! divides n ! ; :: thesis: verum