diff options
| author |  Jason Gross <jagro@google.com> | 2016-06-30 13:24:23 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-06-30 13:24:23 -0700 |
| commit | 6c6c65eff384182197289797ef58ca78bcfff4dc (patch) | |
| tree | be69d58cfb1c90b7bb63047157d7760e4ade63fd /src/Util/NatUtil.v | |
| parent | e8214b0c7f02c23016a4e95734cae813e115de76 (diff) | |
Prove that a ^ k <> 0
Diffstat (limited to 'src/Util/NatUtil.v')
| -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. |