From f2629738a4dfd748a4829323959607ee36e6fd6d Mon Sep 17 00:00:00 2001
From: jadep <jade.philipoom@gmail.com>
Date: Wed, 20 Apr 2016 13:59:33 -0400
Subject: moved lemmas from ModularBaseSystemProofs to various Util files

---
 src/Util/NatUtil.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'src/Util/NatUtil.v')

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.
+
-- 
cgit v1.2.3