diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-04-20 13:59:33 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-04-20 13:59:33 -0400 |
| commit | f2629738a4dfd748a4829323959607ee36e6fd6d (patch) | |
| tree | 7ffd7b5aefdef22e34aea54f97367833f3ff3084 /src/Util/NatUtil.v | |
| parent | b5663bdb42176ac0e808eda16af031c795c22164 (diff) | |
moved lemmas from ModularBaseSystemProofs to various Util files
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. + |