val lemma_pow_one: b:nat -> Lemma (pow 1 b = 1)
let lemma_pow_one b =
  let k = mk_nat_comm_monoid in
  LE.lemma_pow_one k b;
  lemma_pow_nat_is_pow 1 b
val lemma_pow_one: b:nat -> Lemma (pow 1 b = 1)
let lemma_pow_one b =
let k = mk_nat_comm_monoid in
LE.lemma_pow_one k b;
lemma_pow_nat_is_pow 1 b
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.nat Lib.NatMod.lemma_pow_nat_is_pow Prims.unit Lib.Exponentiation.Definition.lemma_pow_one Prims.int Lib.Exponentiation.Definition.comm_monoid Lib.NatMod.mk_nat_comm_monoid
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

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


let rec lemma_pow_ge_zero a b =
  if b = 0 then lemma_pow0 a
  else begin
    lemma_pow_unfold a b;
    lemma_pow_ge_zero a (b - 1) end


let rec lemma_pow_nat_is_pow a b =
  let k = mk_nat_comm_monoid in
  if b = 0 then begin
    lemma_pow0 a;
    LE.lemma_pow0 k a end
  else begin
    lemma_pow_unfold a b;
    lemma_pow_nat_is_pow a (b - 1);
    LE.lemma_pow_unfold k a b;
    () end


let lemma_pow_zero b =
  lemma_pow_unfold 0 b
val lemma_pow_one: b:nat -> Lemma (pow 1 b = 1)
b: Prims.nat -> FStar.Pervasives.Lemma (ensures Lib.NatMod.pow 1 b = 1)