The Coq mailing list

[Andrea Poles <(e6fa90e88c%hidden_head%e6fa90e88c)evilpuchu(e6fa90e88c%hidden_at%e6fa90e88c)gmail.com(e6fa90e88c%hidden_end%e6fa90e88c)>]

Hi all, we need to prove the euclid theorem (on infitite primes) on
natural numbers.
We start writing some definitions and functions but we found many problems.
The divide function is not "compiling":
Require Import Arith.
Open Scope nat_scope.

Definition minus (n m : nat) := n-m.

Fixpoint lwt (n: nat) (m: nat) {struct n}: bool :=

   match n with

      O    =>

        match m with

           O     => false

        | (S m1) => true

        end

   | (S n1) =>

        match m with

           O     =>  false

        | (S m1) => (lwt n1 m1)

        end

   end.

Fixpoint divide (a b:nat) {struct b} : bool :=
match lwt b a with
 true => false
match a with
  O => false
  match b with
    a => true
    | _ => divide a minus(b a)
    end
  end
end.

Divide should return true if b%a =0 false otherwise, but the Coqide
returns "Error: This clause is redundant." on this line:
    | _ => divide a minus(b a).

Do you know why? (consider that we are starting coq in theese days).
Is there anything ready-to-use to prove this theorem ?

Regards,
Andrea.