diff options
Diffstat (limited to 'src/Util/NatUtil.v')
| -rw-r--r-- | src/Util/NatUtil.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 6a62d6c22..1f69b04d2 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -56,3 +56,14 @@ Proof. rewrite <- nat_compare_lt; auto. } Qed. + + + +Lemma beq_nat_eq_nat_dec {R} (x y : nat) (a b : R) + : (if EqNat.beq_nat x y then a else b) = (if eq_nat_dec x y then a else b). +Proof. + destruct (eq_nat_dec x y) as [H|H]; + [ rewrite (proj2 (@beq_nat_true_iff _ _) H); reflexivity + | rewrite (proj2 (@beq_nat_false_iff _ _) H); reflexivity ]. +Qed. + |