diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-20 09:52:27 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-20 09:52:27 -0700 |
| commit | 1f4bd32d809b95612ec0c1682093ca8a4ab50e91 (patch) | |
| tree | 593a5f31c798572916e02c98c837acfd0d37f80d /src/Util/NatUtil.v | |
| parent | 0a4d512d77e34e0d0f5fe4f7711414dd5cd9939e (diff) | |
Add another lemma about +, <= to arith
Diffstat (limited to 'src/Util/NatUtil.v')
| -rw-r--r-- | src/Util/NatUtil.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 3eef976b2..1c144281b 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -5,7 +5,7 @@ Import Nat. Create HintDb natsimplify discriminated. -Hint Resolve mod_bound_pos : arith. +Hint Resolve mod_bound_pos plus_le_compat : arith. Hint Resolve (fun x y p q => proj1 (@Nat.mod_bound_pos x y p q)) (fun x y p q => proj2 (@Nat.mod_bound_pos x y p q)) : arith. Hint Rewrite @mod_small @mod_mod @mod_1_l @mod_1_r succ_pred using omega : natsimplify. |