From 6c6c65eff384182197289797ef58ca78bcfff4dc Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Thu, 30 Jun 2016 13:24:23 -0700
Subject: Prove that a ^ k <> 0

---
 src/Util/NatUtil.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src/Util/NatUtil.v')

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.
-- 
cgit v1.2.3