let ( ! ) n = factorial n
let op_Bang n =
factorial n
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.nat FStar.Math.Fermat.factorial Prims.pos
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)
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;
    }

///
/// Binomial theorem
///

val binomial (n k:nat) : nat
let rec binomial n k =
  match n, k with
  | _, 0 -> 1
  | 0, _ -> 0
  | _, _ -> binomial (n - 1) k + binomial (n - 1) (k - 1)

val binomial_0 (n:nat) : Lemma (binomial n 0 == 1)
let binomial_0 n = ()

val binomial_lt (n:nat) (k:nat{n < k}) : Lemma (binomial n k = 0)
let rec binomial_lt n k =
  match n, k with
  | _, 0 -> ()
  | 0, _ -> ()
  | _ -> binomial_lt (n - 1) k; binomial_lt (n - 1) (k - 1)

val binomial_n (n:nat) : Lemma (binomial n n == 1)
let rec binomial_n n =
  match n with
  | 0 -> ()
  | _ -> binomial_lt n (n + 1); binomial_n (n - 1)

val pascal (n:nat) (k:pos{k <= n}) : Lemma
  (binomial n k + binomial n (k - 1) = binomial (n + 1) k)
let pascal n k = ()

val factorial: nat -> pos
let rec factorial = function
  | 0 -> 1
  | n -> n * factorial (n - 1)
val op_Bang : n: Prims.nat -> Prims.pos
n: Prims.nat -> Prims.pos