diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-08 10:52:11 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-08 10:52:11 -0700 |
| commit | 23b0ea1c4e4ca01f82b1648933f312fba52a1bc7 (patch) | |
| tree | 85c83b04a90d44dc17154c658e08878b22f64a9a /src/Util/NatUtil.v | |
| parent | 51b40b8e143b85b96479be1400016b08699565a3 (diff) | |
Add a NatUtil lemma and db
Diffstat (limited to 'src/Util/NatUtil.v')
| -rw-r--r-- | src/Util/NatUtil.v | 9 |
1 files changed, 9 insertions, 0 deletions
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. |