Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 18 insertions, 3 deletions

diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index a9244455..312b76e9 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: EqNat.v 9966 2007-07-10 23:54:53Z letouzey $ i*)
+(*i $Id$ i*)
 
 (** Equality on natural numbers *)
 
@@ -16,7 +16,7 @@ Implicit Types m n x y : nat.
 
 (** * Propositional equality  *)
 
-Fixpoint eq_nat n m {struct n} : Prop :=
+Fixpoint eq_nat n m : Prop :=
   match n, m with
     | O, O => True
     | O, S _ => False
@@ -68,7 +68,7 @@ Defined.
 
 (** * Boolean equality on [nat] *)
 
-Fixpoint beq_nat n m {struct n} : bool :=
+Fixpoint beq_nat n m : bool :=
   match n, m with
     | O, O => true
     | O, S _ => false
@@ -99,3 +99,18 @@ Lemma beq_nat_false : forall x y, beq_nat x y = false -> x<>y.
 Proof.
  induction x; destruct y; simpl; auto; intros; discriminate.
 Qed.
+
+Lemma beq_nat_true_iff : forall x y, beq_nat x y = true <-> x=y.
+Proof.
+ split. apply beq_nat_true.
+ intros; subst; symmetry; apply beq_nat_refl.
+Qed.
+
+Lemma beq_nat_false_iff : forall x y, beq_nat x y = false <-> x<>y.
+Proof.
+ intros x y.
+ split. apply beq_nat_false.
+ generalize (beq_nat_true_iff x y).
+ destruct beq_nat; auto.
+ intros IFF NEQ. elim NEQ. apply IFF; auto.
+Qed.