From 6e61936ad6058f8cb0f94c79588c58905b2a7055 Mon Sep 17 00:00:00 2001 From: jadep Date: Tue, 9 Aug 2016 13:31:24 -0400 Subject: Convert defined and mostly proven, modulo several admitted lemmas about Z operations and a couple subroutines. --- src/Util/NatUtil.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/Util/NatUtil.v') 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). -- cgit v1.2.3