coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] a claim about prime numbers

From: Stéphane Glondu <steph AT glondu.net>
To: "Flavio L. C. de Moura" <flaviomoura AT unb.br>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] a claim about prime numbers
Date: Sat, 22 May 2010 22:04:53 +0200
Openpgp: id=49881AD3

Flavio L. C. de Moura a écrit :
> 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!

I guess you can by generalizing Euclid's lemma (which is in Znumtheory
as prime_mult).

Cheers,

--
Stéphane

[Coq-Club] a claim about prime numbers, Flavio L. C. de Moura
- Re: [Coq-Club] a claim about prime numbers, Taral
  - Re: [Coq-Club] a claim about prime numbers, Flavio L. C. de Moura
    - Re: [Coq-Club] a claim about prime numbers, St�phane Lescuyer
- Re: [Coq-Club] a claim about prime numbers, Stéphane Glondu
- [Coq-Club] Re: a claim about prime numbers, Adam Megacz