let bn_mont_t (#t:limb_t) (#len:BN.bn_len t) (n:lbignum t len) =
  x:lbignum t len{bn_v x < bn_v n}
let bn_mont_t (#t: limb_t) (#len: BN.bn_len t) (n: lbignum t len) =
x: lbignum t len {bn_v x < bn_v n}
Hacl.Spec.Bignum.MontExponentiation.fst.checked
Spec.Exponentiation.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.NatMod.fsti.checked Lib.IntTypes.fsti.checked Lib.Exponentiation.fsti.checked Hacl.Spec.Montgomery.Lemmas.fst.checked Hacl.Spec.Exponentiation.Lemmas.fst.checked Hacl.Spec.Bignum.Montgomery.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Spec.Bignum.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Hacl.Spec.Bignum.MontExponentiation.fst
Hacl.Spec.Bignum.Definitions.limb_t Hacl.Spec.Bignum.bn_len Hacl.Spec.Bignum.Definitions.lbignum Prims.b2t Prims.op_LessThan Hacl.Spec.Bignum.Definitions.bn_v
module Hacl.Spec.Bignum.MontExponentiation

open FStar.Mul

open Lib.IntTypes
open Lib.Sequence

open Hacl.Spec.Bignum.Definitions

module LE = Lib.Exponentiation
module SE = Spec.Exponentiation

module E = Hacl.Spec.Exponentiation.Lemmas
module M = Hacl.Spec.Montgomery.Lemmas

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

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

// All operations are performed in the Montgomery domain!

unfold
val bn_mont_t : n: Hacl.Spec.Bignum.Definitions.lbignum t len -> Type0
n: Hacl.Spec.Bignum.Definitions.lbignum t len -> Type0