let bn_mont_pre (#t:limb_t) (#nLen:size_pos) (n:lbignum t nLen) (mu:limb t) =
  (1 + bn_v n * v mu) % pow2 (bits t) == 0 /\
  bn_v n % 2 = 1 /\ 1 < bn_v n /\
  bn_v n < pow2 (bits t * nLen)
let bn_mont_pre (#t: limb_t) (#nLen: size_pos) (n: lbignum t nLen) (mu: limb t) =
(1 + bn_v n * v mu) % pow2 (bits t) == 0 /\ bn_v n % 2 = 1 /\ 1 < bn_v n /\
bn_v n < pow2 (bits t * nLen)
Hacl.Spec.Bignum.Montgomery.fsti.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.Montgomery.Lemmas.fst.checked Hacl.Spec.Bignum.Definitions.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Hacl.Spec.Bignum.Montgomery.fsti
Hacl.Spec.Bignum.Definitions.limb_t Lib.IntTypes.size_pos Hacl.Spec.Bignum.Definitions.lbignum Hacl.Spec.Bignum.Definitions.limb Prims.l_and Prims.eq2 Prims.int Prims.op_Modulus Prims.op_Addition FStar.Mul.op_Star Hacl.Spec.Bignum.Definitions.bn_v Lib.IntTypes.v Lib.IntTypes.SEC Prims.pow2 Lib.IntTypes.bits Prims.b2t Prims.op_Equality Prims.op_LessThan Prims.logical
module Hacl.Spec.Bignum.Montgomery

open FStar.Mul

open Lib.IntTypes
open Lib.Sequence

open Hacl.Spec.Bignum.Definitions
module M = Hacl.Spec.Montgomery.Lemmas

#reset-options "--z3rlimit 50 --fuel 0 --ifuel 0"
val bn_mont_pre : n: Hacl.Spec.Bignum.Definitions.lbignum t nLen -> mu: Hacl.Spec.Bignum.Definitions.limb t
  -> Prims.logical
n: Hacl.Spec.Bignum.Definitions.lbignum t nLen -> mu: Hacl.Spec.Bignum.Definitions.limb t
  -> Prims.logical