val lemma_pow_double: a:int -> b:nat -> Lemma (pow (a * a) b == pow a (b + b))
let lemma_pow_double a b =
  let k = mk_nat_comm_monoid in
  LE.lemma_pow_double k a b;
  lemma_pow_nat_is_pow (a * a) b;
  lemma_pow_nat_is_pow a (b + b)
val lemma_pow_double: a:int -> b:nat -> Lemma (pow (a * a) b == pow a (b + b))
let lemma_pow_double a b =
let k = mk_nat_comm_monoid in
LE.lemma_pow_double k a b;
lemma_pow_nat_is_pow (a * a) b;
lemma_pow_nat_is_pow a (b + 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.int Prims.nat Lib.NatMod.lemma_pow_nat_is_pow Prims.op_Addition Prims.unit FStar.Mul.op_Star Lib.Exponentiation.Definition.lemma_pow_double 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


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


let lemma_pow_add x n m =
  let k = mk_nat_comm_monoid in
  LE.lemma_pow_add k x n m;
  lemma_pow_nat_is_pow x n;
  lemma_pow_nat_is_pow x m;
  lemma_pow_nat_is_pow x (n + m)


let lemma_pow_mul x n m =
  let k = mk_nat_comm_monoid in
  LE.lemma_pow_mul k x n m;
  lemma_pow_nat_is_pow x n;
  lemma_pow_nat_is_pow (pow x n) m;
  lemma_pow_nat_is_pow x (n * m)
val lemma_pow_double: a:int -> b:nat -> Lemma (pow (a * a) b == pow a (b + b))
a: Prims.int -> b: Prims.nat
  -> FStar.Pervasives.Lemma (ensures Lib.NatMod.pow (a * a) b == Lib.NatMod.pow a (b + b))