The Coq mailing list

[Adam Megacz <megacz AT cs.berkeley.edu>]

Small hint: since you're dealing only with positive numbers here, you'll
have a much easier time using nat rather than Z.  Instead of writing

    forall n i k, ... n-i+k ...

try 

    forall n i k m, m+i=n -> ... m+k ...

this way you'll have an easier time with the inductions.

"Flavio L. C. de Moura" 
<flaviomoura AT unb.br>
 writes:
> I am afraid this theorem cannot be proved in Coq because in a certain
> sense we cannot find the exact k such that i divides (n-i+k) (1<=k<i)...
> is that true?

You'll want to show that if [i] divides the big product it divides one
of the multiplicands.  Prove this by induction on the number of
multiplicands (here's another place where working with nat will make
your life easier).

Then show that if the difference between two numbers is strictly less
than "i", it cannot be the case that "i" divides both of them.  Then
show that if "i" divided your big product, it would divide one of the
terms of the product, and the difference between any of them and "n" is
strictly less than "i".

  - a