diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-07-25 22:41:08 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-07-25 22:41:08 -0400 |
| commit | a8836bda7dc57933098fe5d513a52221591252b0 (patch) | |
| tree | f86ddaf0f075ae357a852be408c51e9d6a34200b /src/Util/NatUtil.v | |
| parent | 4c73b7273c5fae67154ad9dd8bd3a719e4fbcf5f (diff) | |
Fix 8.4 build.
Diffstat (limited to 'src/Util/NatUtil.v')
| -rw-r--r-- | src/Util/NatUtil.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 84fbb11eb..bf485d0d0 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -64,9 +64,10 @@ Proof. reflexivity. Qed. -Lemma pred_mod : forall m, (0 < m)%nat -> ((pred m) mod m)%nat = Init.Nat.pred m. +Lemma pred_mod : forall m, (0 < m)%nat -> ((pred m) mod m)%nat = pred m. Proof. - intros; apply Nat.mod_small; omega. + intros; apply Nat.mod_small. + destruct m; try omega; rewrite Nat.pred_succ; auto. Qed. Lemma div_add_l' : forall a b c, a <> 0 -> (a * b + c) / a = b + c / a. |