The Coq mailing list

[Andrea Poles <evilpuchu AT gmail.com>]

Hi all, we have modified the coq-implementation of the Euclid's
theorem (for primes).
The following code is supposed to be right:

  1 Require Import Wf_nat.
  2 Require Import Coq.Program.Equality.
  3
  4
  5 Variable Pn1 : nat.
  6 Definition Divides (n m : nat) : Prop := exists q : nat, m = n * q.
  7 Definition Prime (n : nat) : Prop :=
  8   n > 1 /\ (forall q : nat, Divides q n -> q = 1 \/ q = n).
  9
 10 Fixpoint fact (n:nat) : nat :=
 11   match n with
 12     | O => 1
 13     | S n => S n * fact n
 14   end.
 15 Definition Bound := forall (Pn:nat) , Prime(Pn) -> (exists x:nat , (gt x 
Pn)
 16                         /\ x < fact(Pn)+1
 17                         /\ Prime(x)).
 18
 19 Hypothesis  hyp: Prime Pn1.
 20
 21 Theorem Euclide : forall (y:nat) ,
 22        (exists x:nat , Prime(x) /\ (gt x y)).
 23 intros.
 24 elim y.
 25 exists Pn1.
 26 split.
 27 apply hyp.

Now, we have to demonstrate that primes are infinitely, using the
above "rules"... and the Euclid's theorem of course!
Any idea?

Thank you all!