(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.3                                 *)
(*                               July 1st 1999                              *)
(*                                                                          *)
(****************************************************************************)
(*                                 EqNat.v                                  *)
(****************************************************************************)

(**************************************************************************)
(*                    Equality on natural numbers                         *)
(**************************************************************************)

Fixpoint  eq_nat [n:nat] : nat -> Prop :=
  [m:nat]Cases n m of 
                O      O     => True
             |  O     (S _)  => False
             | (S _)   O     => False
             | (S n1) (S m1) => (eq_nat n1 m1)
          end.

Theorem eq_nat_refl : (n:nat)(eq_nat n n).
Induction n; Simpl; Auto.
Qed.
Hints Resolve eq_nat_refl : arith v62.

Theorem eq_eq_nat : (n,m:nat)(n=m)->(eq_nat n m).
Induction 1; Trivial with arith.
Qed.
Hints Immediate eq_eq_nat : arith v62.

Theorem eq_nat_eq : (n,m:nat)(eq_nat n m)->(n=m).
Induction n; Induction m; Simpl; (Contradiction Orelse Auto with arith).
Qed.
Hints Immediate eq_nat_eq : arith v62.

Theorem eq_nat_elim : (n:nat)(P:nat->Prop)(P n)->(m:nat)(eq_nat n m)->(P m).
Intros; Replace m with n; Auto with arith.
Qed.

Theorem eq_nat_decide : (n,m:nat){(eq_nat n m)}+{~(eq_nat n m)}.
Induction n.
Destruct m.
Auto with arith.
(Intro; Right; Red; Trivial with arith).
Destruct m.
(Right; Red; Auto with arith).
Intros.
Simpl.
Apply H.
Defined.

Fixpoint  beq_nat [n:nat] : nat -> bool :=
  [m:nat]Cases n m of 
                O      O     => true
             |  O     (S _)  => false
             | (S _)   O     => false
             | (S n1) (S m1) => (beq_nat n1 m1)
          end.


(* $Id: EqNat.v,v 1.9 1999/06/29 07:48:32 loiseleu Exp $ *)
