val lemma_pow_mod_base: a:int -> b:nat -> n:pos -> Lemma (pow a b % n == pow (a % n) b % n)
let rec lemma_pow_mod_base a b n =
  if b = 0 then begin
    lemma_pow0 a;
    lemma_pow0 (a % n) end
  else begin
    calc (==) {
      pow a b % n;
      (==) { lemma_pow_unfold a b }
      a * pow a (b - 1) % n;
      (==) { Math.Lemmas.lemma_mod_mul_distr_r a (pow a (b - 1)) n }
      a * (pow a (b - 1) % n) % n;
      (==) { lemma_pow_mod_base a (b - 1) n }
      a * (pow (a % n) (b - 1) % n) % n;
      (==) { Math.Lemmas.lemma_mod_mul_distr_r a (pow (a % n) (b - 1)) n }
      a * pow (a % n) (b - 1) % n;
      (==) { Math.Lemmas.lemma_mod_mul_distr_l a (pow (a % n) (b - 1)) n }
      a % n * pow (a % n) (b - 1) % n;
      (==) { lemma_pow_unfold (a % n) b }
      pow (a % n) b % n;
    };
    assert (pow a b % n == pow (a % n) b % n)
  end
val lemma_pow_mod_base: a:int -> b:nat -> n:pos -> Lemma (pow a b % n == pow (a % n) b % n)
let rec lemma_pow_mod_base a b n =
if b = 0
then
  (lemma_pow0 a;
    lemma_pow0 (a % n))
else
  (calc ( == ) {
      pow a b % n;
      ( == ) { lemma_pow_unfold a b }
      a * pow a (b - 1) % n;
      ( == ) { Math.Lemmas.lemma_mod_mul_distr_r a (pow a (b - 1)) n }
      a * (pow a (b - 1) % n) % n;
      ( == ) { lemma_pow_mod_base a (b - 1) n }
      a * (pow (a % n) (b - 1) % n) % n;
      ( == ) { Math.Lemmas.lemma_mod_mul_distr_r a (pow (a % n) (b - 1)) n }
      a * pow (a % n) (b - 1) % n;
      ( == ) { Math.Lemmas.lemma_mod_mul_distr_l a (pow (a % n) (b - 1)) n }
      (a % n) * pow (a % n) (b - 1) % n;
      ( == ) { lemma_pow_unfold (a % n) b }
      pow (a % n) b % n;
    };
    assert (pow a b % n == pow (a % n) b % n))
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 Prims.pos Prims.op_Equality Lib.NatMod.lemma_pow0 Prims.op_Modulus Prims.unit Prims.bool Prims._assert Prims.eq2 Lib.NatMod.pow FStar.Calc.calc_finish Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step FStar.Mul.op_Star Prims.op_Subtraction FStar.Calc.calc_init FStar.Calc.calc_pack Lib.NatMod.lemma_pow_unfold Prims.squash FStar.Math.Lemmas.lemma_mod_mul_distr_r Lib.NatMod.lemma_pow_mod_base FStar.Math.Lemmas.lemma_mod_mul_distr_l
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)


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)


let lemma_pow_mul_base a b n =
  let k = mk_nat_comm_monoid in
  LE.lemma_pow_mul_base k a b n;
  lemma_pow_nat_is_pow a n;
  lemma_pow_nat_is_pow b n;
  lemma_pow_nat_is_pow (a * b) n
val lemma_pow_mod_base: a:int -> b:nat -> n:pos -> Lemma (pow a b % n == pow (a % n) b % n)
a: Prims.int -> b: Prims.nat -> n: Prims.pos
  -> FStar.Pervasives.Lemma (ensures Lib.NatMod.pow a b % n == Lib.NatMod.pow (a % n) b % n)