diff options
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. |