diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-08-09 13:31:24 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-08-09 13:31:24 -0400 |
| commit | 6e61936ad6058f8cb0f94c79588c58905b2a7055 (patch) | |
| tree | 46350c68afb9366314f9555eddcf9a075bf8bff6 /src/Util/NatUtil.v | |
| parent | 1039bec0ad627d0950c83fdd77403cb86ceccff5 (diff) | |
Convert defined and mostly proven, modulo several admitted lemmas about Z operations and a couple subroutines.
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). |