let qmont_as_nat (h:mem) (a:felem) = SM.from_qmont (as_nat h a)
let qmont_as_nat (h: mem) (a: felem) =
SM.from_qmont (as_nat h a)
Hacl.Impl.P256.Scalar.fsti.checked
Spec.P256.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.P256.Montgomery.fsti.checked Hacl.Impl.P256.Bignum.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.P256.Scalar.fsti
FStar.Monotonic.HyperStack.mem Hacl.Impl.P256.Bignum.felem Hacl.Spec.P256.Montgomery.from_qmont Hacl.Impl.P256.Bignum.as_nat Spec.P256.PointOps.qelem
module Hacl.Impl.P256.Scalar

open FStar.Mul
open FStar.HyperStack.All
open FStar.HyperStack
module ST = FStar.HyperStack.ST

open Lib.IntTypes
open Lib.Buffer

open Hacl.Impl.P256.Bignum

module S = Spec.P256
module SM = Hacl.Spec.P256.Montgomery
module BSeq = Lib.ByteSequence

#set-options "--z3rlimit 30 --fuel 0 --ifuel 0"
val qmont_as_nat : h: FStar.Monotonic.HyperStack.mem -> a: Hacl.Impl.P256.Bignum.felem
  -> Prims.GTot Spec.P256.PointOps.qelem
h: FStar.Monotonic.HyperStack.mem -> a: Hacl.Impl.P256.Bignum.felem
  -> Prims.GTot Spec.P256.PointOps.qelem