val pow (a: int) (k: nat) : int
let rec pow (a:int) (k:nat) : int =
  if k = 0 then 1
  else a * pow a (k - 1)
val pow (a: int) (k: nat) : int
let rec pow (a: int) (k: nat) : int =
if k = 0 then 1 else a * pow a (k - 1)
FStar.Math.Fermat.fsti.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Euclid.fsti.checked
FStar.Math.Fermat.fsti
Prims.int Prims.nat Prims.op_Equality Prims.bool FStar.Mul.op_Star FStar.Math.Fermat.pow Prims.op_Subtraction
module FStar.Math.Fermat

open FStar.Mul
open FStar.Math.Euclid

/// Fermat's Little Theorem (and Binomial Theorem)
///
/// Proven by induction from the Freshman's dream identity
///
///   pow (a + b) p % p = (pow a p + pow b p) % p
///
/// which follows from the Binomial Theorem
///
///   pow (a + b) n = sum_{i=0}^n (binomial n k * pow a (n - i) * pow b i)
///
/// which in turn can be proved by induction from Pascal's identity
///
///   binomial n k + binomial n (k - 1) = binomial (n + 1) k
///
/// See
///  https://github.com/coqtail/coqtail/blob/master/src/Hierarchy/Commutative_ring_binomial.v
///  https://github.com/coq-contribs/rsa/blob/master/Binomials.v
///

#set-options "--fuel 0 --ifuel 0"
val pow (a: int) (k: nat) : int
a: Prims.int -> k: Prims.nat -> Prims.int