1 files changed, 78 insertions, 0 deletions
diff --git a/theories7/Arith/EqNat.v b/theories7/Arith/EqNat.v
new file mode 100755
index 00000000..9f5ee7ee
--- /dev/null
+++ b/theories7/Arith/EqNat.v
@@ -0,0 +1,78 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: EqNat.v,v 1.1.2.1 2004/07/16 19:31:24 herbelin Exp $ i*)
+
+(** Equality on natural numbers *)
+
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
+
+Implicit Variables Type m,n,x,y:nat.
+
+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).
+NewInduction n; Simpl; Auto.
+Qed.
+Hints Resolve eq_nat_refl : arith v62.
+
+Theorem eq_eq_nat : (n,m:nat)(n=m)->(eq_nat n m).
+NewInduction 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).
+NewInduction n; NewInduction 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)}.
+NewInduction n.
+NewDestruct m.
+Auto with arith.
+Intros; Right; Red; Trivial with arith.
+NewDestruct m.
+Right; Red; Auto with arith.
+Intros.
+Simpl.
+Apply IHn.
+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.
+
+Lemma beq_nat_refl : (x:nat)true=(beq_nat x x).
+Proof.
+  Intro x; NewInduction x; Simpl; Auto.
+Qed.
+
+Definition beq_nat_eq : (x,y:nat)true=(beq_nat x y)->x=y.
+Proof.
+  Double Induction x y; Simpl.
+    Reflexivity.
+    Intros; Discriminate H0.
+    Intros; Discriminate H0.
+    Intros; Case (H0 ? H1); Reflexivity.
+Defined.
+