From 1f4bd32d809b95612ec0c1682093ca8a4ab50e91 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 20 Jul 2016 09:52:27 -0700 Subject: Add another lemma about +, <= to arith --- src/Util/NatUtil.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util/NatUtil.v') 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. -- cgit v1.2.3