diff options
| -rw-r--r-- | src/Util/NatUtil.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index bc2c8425b..0cdfd784f 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -1,4 +1,5 @@ Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega. +Require Import Coq.micromega.Psatz. Import Nat. Local Open Scope nat_scope. @@ -78,3 +79,10 @@ Proof. [ rewrite (proj2 (@beq_nat_true_iff _ _) H); reflexivity | rewrite (proj2 (@beq_nat_false_iff _ _) H); reflexivity ]. Qed. + +Lemma pow_nonzero a k : a <> 0 -> a ^ k <> 0. +Proof. + intro; induction k; simpl; nia. +Qed. + +Hint Resolve pow_nonzero : arith. |