val lemma_pow_gt_zero: a:pos -> b:nat -> Lemma (pow a b > 0) [SMTPat (pow a b)]
let rec lemma_pow_gt_zero a b =
  if b = 0 then lemma_pow0 a
  else begin
    lemma_pow_unfold a b;
    lemma_pow_gt_zero a (b - 1) end
val lemma_pow_gt_zero: a:pos -> b:nat -> Lemma (pow a b > 0) [SMTPat (pow a b)]
let rec lemma_pow_gt_zero a b =
if b = 0
then lemma_pow0 a
else
  (lemma_pow_unfold a b;
    lemma_pow_gt_zero a (b - 1))
Lib.NatMod.fst.checked
prims.fst.checked Lib.Exponentiation.Definition.fsti.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Lib.NatMod.fst
Prims.pos Prims.nat Prims.op_Equality Prims.int Lib.NatMod.lemma_pow0 Prims.bool Lib.NatMod.lemma_pow_gt_zero Prims.op_Subtraction Prims.unit Lib.NatMod.lemma_pow_unfold
module Lib.NatMod

module LE = Lib.Exponentiation.Definition

#set-options "--z3rlimit 30 --fuel 0 --ifuel 0"

#push-options "--fuel 2"
let lemma_pow0 a = ()

let lemma_pow1 a = ()

let lemma_pow_unfold a b = ()
#pop-options
val lemma_pow_gt_zero: a:pos -> b:nat -> Lemma (pow a b > 0) [SMTPat (pow a b)]
a: Prims.pos -> b: Prims.nat
  -> FStar.Pervasives.Lemma (ensures Lib.NatMod.pow a b > 0) [SMTPat (Lib.NatMod.pow a b)]