The Coq mailing list

["Flavio L. C. de Moura" <flaviomoura AT unb.br>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hi Coq users,

 I am working on a development in Coq and I reached a point where I need
to prove that if a prime number i divides the product
(n-i+1).(n-i+2)...(n-1) then i doesn't divide n. Precisely the product
is defined by

Fixpoint prod_in (n m:nat) {struct m} :=
  match n with
    | 0%nat => 0%nat
    | S j =>   match m with
                 | 0%nat => 0%nat
                 | S i =>
                   match (le_gt_dec i j) with
                     | right _ => mult m (prod_in n i)
                     | _ => m
                   end
               end
  end.

The main theorem is:

Theorem not_div_n: forall (n i:Z), 1 < i < n -> prime i -> (i |
Z_of_nat(prod_in (Zabs_nat(n-i+1)) (Zabs_nat(n-1)))) -> ~(i|n).

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? Any comments is very welcome!

Cheers,
Flávio.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.15 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAkv4JCwACgkQJ9M3XSenoWgWWACfa2oY0dPW9iNCbt0br8+IzxH9
jjAAoJS5v9yUUau6S7RAzJ++xvUGvlGR
=Gz/E
-----END PGP SIGNATURE-----