diff options
Diffstat (limited to 'theories/Arith/EqNat.v')
| -rw-r--r-- | theories/Arith/EqNat.v | 21 |
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. |