val mod_inv_prime_lemma: n:nat{1 < n /\ Euclid.is_prime n} -> a:pos{a < n} ->
  Lemma (Lib.NatMod.pow_mod #n a (n - 2) * a % n = 1)
let mod_inv_prime_lemma n a =
  Math.Lemmas.small_mod a n;
  assert (a == a % n);
  assert (a <> 0 /\ a % n <> 0);

  calc (==) {
    Lib.NatMod.pow_mod #n a (n - 2) * a % n;
    (==) { Lib.NatMod.lemma_pow_mod #n a (n - 2) }
    Lib.NatMod.pow a (n - 2) % n * a % n;
    (==) { Math.Lemmas.lemma_mod_mul_distr_l (Lib.NatMod.pow a (n - 2)) a n }
    Lib.NatMod.pow a (n - 2) * a % n;
    (==) { Lib.NatMod.lemma_pow1 a; Lib.NatMod.lemma_pow_add a (n - 2) 1 }
    Lib.NatMod.pow a (n - 1) % n;
    (==) { pow_eq a (n - 1) }
    Fermat.pow a (n - 1) % n;
    (==) { Fermat.fermat_alt n a }
    1;
    }
val mod_inv_prime_lemma: n:nat{1 < n /\ Euclid.is_prime n} -> a:pos{a < n} ->
  Lemma (Lib.NatMod.pow_mod #n a (n - 2) * a % n = 1)
let mod_inv_prime_lemma n a =
Math.Lemmas.small_mod a n;
assert (a == a % n);
assert (a <> 0 /\ a % n <> 0);
calc ( == ) {
  Lib.NatMod.pow_mod #n a (n - 2) * a % n;
  ( == ) { Lib.NatMod.lemma_pow_mod #n a (n - 2) }
  (Lib.NatMod.pow a (n - 2) % n) * a % n;
  ( == ) { Math.Lemmas.lemma_mod_mul_distr_l (Lib.NatMod.pow a (n - 2)) a n }
  Lib.NatMod.pow a (n - 2) * a % n;
  ( == ) { (Lib.NatMod.lemma_pow1 a;
    Lib.NatMod.lemma_pow_add a (n - 2) 1) }
  Lib.NatMod.pow a (n - 1) % n;
  ( == ) { pow_eq a (n - 1) }
  Fermat.pow a (n - 1) % n;
  ( == ) { Fermat.fermat_alt n a }
  1;
}
Hacl.Spec.Bignum.ModInv.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.NatMod.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.Bignum.Montgomery.fsti.checked Hacl.Spec.Bignum.Exponentiation.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Spec.Bignum.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Math.Fermat.fsti.checked FStar.Math.Euclid.fsti.checked FStar.Calc.fsti.checked
Hacl.Spec.Bignum.ModInv.fst
Prims.nat Prims.l_and Prims.b2t Prims.op_LessThan FStar.Math.Euclid.is_prime Prims.pos FStar.Calc.calc_finish Prims.int Prims.eq2 Prims.op_Modulus FStar.Mul.op_Star Lib.NatMod.pow_mod Prims.op_Subtraction Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step FStar.Math.Fermat.pow Lib.NatMod.pow FStar.Calc.calc_init FStar.Calc.calc_pack Lib.NatMod.lemma_pow_mod Prims.squash FStar.Math.Lemmas.lemma_mod_mul_distr_l Lib.NatMod.lemma_pow_add Lib.NatMod.lemma_pow1 Hacl.Spec.Bignum.ModInv.pow_eq FStar.Math.Fermat.fermat_alt Prims._assert Prims.op_disEquality FStar.Math.Lemmas.small_mod
module Hacl.Spec.Bignum.ModInv

open FStar.Mul

open Lib.IntTypes
open Lib.Sequence
open Lib.LoopCombinators

open Hacl.Spec.Bignum.Definitions
open Hacl.Spec.Bignum

module Fermat = FStar.Math.Fermat
module Euclid = FStar.Math.Euclid

module BE = Hacl.Spec.Bignum.Exponentiation
module BM = Hacl.Spec.Bignum.Montgomery
module BN = Hacl.Spec.Bignum

#reset-options "--z3rlimit 50 --fuel 0 --ifuel 0"

#push-options "--fuel 1"
val pow_eq: a:nat -> n:nat -> Lemma (Fermat.pow a n == Lib.NatMod.pow a n)
let rec pow_eq a n =
  if n = 0 then ()
  else pow_eq a (n - 1)
#pop-options

val mod_inv_prime_lemma: n:nat{1 < n /\ Euclid.is_prime n} -> a:pos{a < n} ->
  Lemma (Lib.NatMod.pow_mod #n a (n - 2) * a % n = 1)
val mod_inv_prime_lemma: n:nat{1 < n /\ Euclid.is_prime n} -> a:pos{a < n} ->
  Lemma (Lib.NatMod.pow_mod #n a (n - 2) * a % n = 1)
n: Prims.nat{1 < n /\ FStar.Math.Euclid.is_prime n} -> a: Prims.pos{a < n}
  -> FStar.Pervasives.Lemma (ensures Lib.NatMod.pow_mod a (n - 2) * a % n = 1)