The Coq mailing list

[Patricia Peratto <psperatto AT vera.com.uy>]

I want to prove (using nat_ind) the following proposition.

I adjoin the proof I have written myself.

Definition aux1b (n:nat) : forall m:nat,
                           forall (e:n=m),S n = S m.
nat_ind (fun n:nat =>
         (forall m:nat, forall e:n=m, S n = S m))

         (fun m:nat, fun e:O=m,
            (f_equal nat nat S O m e))

         (fun p:nat, fun q:(forall m:nat,
              forall e:p = m, S p = S m) =>
              (fun m2:nat =>
                      (fun e2:(S p)=m2 =>
                   (f_equal nat nat S (S p) m2 e2))))
          n.

I have proved it  using "induction" but I want to

find the proof using nat_ind.

I have gotten the following message:

Error: The reference nat_ind was not found in the current environment.

Someone can say me where I'm wrong?

Regards

Patricia