val pow_mod (p:pos) (a:int) (k:nat) : Lemma (pow a k % p == pow (a % p) k % p)
let rec pow_mod p a k =
  if k = 0 then ()
  else
    calc (==) {
      pow a k % p;
      == { }
      a * pow a (k - 1) % p;
      == { lemma_mod_mul_distr_r a (pow a (k - 1)) p }
      (a * (pow a (k - 1) % p)) % p;
      == { pow_mod p a (k - 1) }
      (a * (pow (a % p) (k - 1) % p)) % p;
      == { lemma_mod_mul_distr_r a (pow (a % p) (k - 1)) p }
      a * pow (a % p) (k - 1) % p;
      == { lemma_mod_mul_distr_l a (pow (a % p) (k - 1)) p }
      (a % p * pow (a % p) (k - 1)) % p;
      == { }
      pow (a % p) k % p;
    }
val pow_mod (p:pos) (a:int) (k:nat) : Lemma (pow a k % p == pow (a % p) k % p)
let rec pow_mod p a k =
if k = 0
then ()
else
  calc ( == ) {
    pow a k % p;
    ( == ) { () }
    a * pow a (k - 1) % p;
    ( == ) { lemma_mod_mul_distr_r a (pow a (k - 1)) p }
    (a * (pow a (k - 1) % p)) % p;
    ( == ) { pow_mod p a (k - 1) }
    (a * (pow (a % p) (k - 1) % p)) % p;
    ( == ) { lemma_mod_mul_distr_r a (pow (a % p) (k - 1)) p }
    a * pow (a % p) (k - 1) % p;
    ( == ) { lemma_mod_mul_distr_l a (pow (a % p) (k - 1)) p }
    ((a % p) * pow (a % p) (k - 1)) % p;
    ( == ) { () }
    pow (a % p) k % p;
  }
FStar.Math.Fermat.fst.checked
prims.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Math.Euclid.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
FStar.Math.Fermat.fst
Prims.pos Prims.int Prims.nat Prims.op_Equality Prims.bool FStar.Calc.calc_finish Prims.eq2 Prims.op_Modulus FStar.Math.Fermat.pow Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step FStar.Mul.op_Star Prims.op_Subtraction FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash FStar.Math.Lemmas.lemma_mod_mul_distr_r FStar.Math.Fermat.pow_mod FStar.Math.Lemmas.lemma_mod_mul_distr_l
module FStar.Math.Fermat

open FStar.Mul
open FStar.Math.Lemmas
open FStar.Math.Euclid

#set-options "--fuel 1 --ifuel 0 --z3rlimit 20"

///
/// Pow
///

val pow_zero (k:pos) : Lemma (ensures pow 0 k == 0) (decreases k)
let rec pow_zero k =
  match k with
  | 1 -> ()
  | _ -> pow_zero (k - 1)

val pow_one (k:nat) : Lemma (pow 1 k == 1)
let rec pow_one = function
  | 0 -> ()
  | k -> pow_one (k - 1)

val pow_plus (a:int) (k m:nat): Lemma (pow a (k + m) == pow a k * pow a m)
let rec pow_plus a k m =
  match k with
  | 0 -> ()
  | _ ->
    calc (==) {
      pow a (k + m);
      == { }
      a * pow a ((k + m) - 1);
      == { pow_plus a (k - 1) m }
      a * (pow a (k - 1) * pow a m);
      == { }
      pow a k * pow a m;
    }

val pow_mod (p:pos) (a:int) (k:nat) : Lemma (pow a k % p == pow (a % p) k % p)
val pow_mod (p:pos) (a:int) (k:nat) : Lemma (pow a k % p == pow (a % p) k % p)
p: Prims.pos -> a: Prims.int -> k: Prims.nat
  -> FStar.Pervasives.Lemma
    (ensures FStar.Math.Fermat.pow a k % p == FStar.Math.Fermat.pow (a % p) k % p)