diff options
Diffstat (limited to 'src/Util/NatUtil.v')
-rw-r--r-- | src/Util/NatUtil.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index bf485d0d0..5c65148c0 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -10,6 +10,8 @@ Hint Resolve (fun x y p q => proj1 (@Nat.mod_bound_pos x y p q)) (fun x y p q => Hint Rewrite @mod_small @mod_mod @mod_1_l @mod_1_r succ_pred using omega : natsimplify. +Hint Rewrite sub_diag add_0_l add_0_r sub_0_r : natsimplify. + Local Open Scope nat_scope. Lemma min_def {x y} : min x y = x - (x - y). |