This answer completely formalizes the argument of Nurdin Takenov in a manner sufficient to easily be expressed in an automated theorem prover such as PVS. Note that this proof uses strong induction on the sum m+k to avoid any nasty double inductions, and is explicit about all assumptions on the arguments:
DEFINITION: *P*roduct of k consecutive posints starting at m (m>=1, k>=1)
i.e. P(m,k) ==def== m...(m+k-1)
LEMMA: P(m,k) = k*P(m,k-1) + P(m-1,k) if m>=2 and k>=2
PROOF: P(m,k) = m...(m+k-1)
= m...(m+k-2)[ k + (m-1) ]
= k*(m)...(m+k-2) + (m-1)...(m+k-2)
= k*P(m,k-1) + P(m-1,k) QED
THEOREM: Product of k consecutive posints starting with m is divisible by k factorial
i.e. k! | P(m,k)
PROOF (by strong induction on all sums m+k <= n):
(i) BASIS: If n = 2 then clearly m=k=1 and we have k! = 1! clearly divides P(m,k) = 1
(ii) INDUCTION STEP: Assume k! | P(m,k) for all m+k<=n. Now to show that k! | P(m,k) for all m+k <= n+1
If m=1 we are done since P(1,k) = 1...k = k! and if k=1 then k! = 1! clearly divides P(m,k). So in the remainder
we may assume that m >= 2 and k >= 2. Also if m+k<=n we are done vacuously, so consider only that m+k = n+1.
By the lemma we have P(m,k) = k*P(m,k-1) + P(m-1,k) so by the Induction hypothesis we have (k-1)! | P(m,k-1)
and thus also k! | k*P(m,k-1) and also by the Induction hypothesis k! | P(m-1,k) and finally k! | P(m,k) QED