From 23b0ea1c4e4ca01f82b1648933f312fba52a1bc7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 8 Jul 2016 10:52:11 -0700 Subject: Add a NatUtil lemma and db --- src/Util/NatUtil.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'src/Util/NatUtil.v') diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 2dd1ce6b5..c8a6e8247 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -2,6 +2,10 @@ Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega. Require Import Coq.micromega.Psatz. Import Nat. +Create HintDb natsimplify discriminated. + +Hint Rewrite @Nat.mod_small using omega : natsimplify. + Local Open Scope nat_scope. Lemma min_def {x y} : min x y = x - (x - y). @@ -129,3 +133,8 @@ Proof. Qed. Hint Resolve pow_nonzero : arith. + +Lemma mod_same_eq a b : a <> 0 -> a = b -> b mod a = 0. +Proof. intros; subst; apply mod_same; assumption. Qed. + +Hint Rewrite @mod_same_eq using omega : natsimplify. -- cgit v1.2.3