val store_felem5_lemma: f:felem5 -> Lemma
  (requires felem_fits5 f (1,1,1,1,1))
  (ensures  as_nat4 (store_felem5 f) == as_nat5 f)
let store_felem5_lemma f =
  L1.store_felem5_lemma f
val store_felem5_lemma: f:felem5 -> Lemma
  (requires felem_fits5 f (1,1,1,1,1))
  (ensures  as_nat4 (store_felem5 f) == as_nat5 f)
let store_felem5_lemma f =
L1.store_felem5_lemma f
Hacl.Spec.K256.Field52.Lemmas.fst.checked
Spec.K256.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Hacl.Spec.K256.MathLemmas.fst.checked Hacl.Spec.K256.Field52.Lemmas3.fst.checked Hacl.Spec.K256.Field52.Lemmas2.fst.checked Hacl.Spec.K256.Field52.Lemmas1.fst.checked Hacl.Spec.K256.Field52.Definitions.Lemmas.fst.checked Hacl.Spec.K256.Field52.Definitions.fst.checked Hacl.Spec.K256.Field52.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Hacl.Spec.K256.Field52.Lemmas.fst
Hacl.Spec.K256.Field52.Definitions.felem5 Hacl.Spec.K256.Field52.Lemmas1.store_felem5_lemma Prims.unit
module Hacl.Spec.K256.Field52.Lemmas

open FStar.Mul
open Lib.IntTypes

module S = Spec.K256

include Hacl.Spec.K256.Field52.Definitions
include Hacl.Spec.K256.Field52

module ML = Hacl.Spec.K256.MathLemmas
module LD = Hacl.Spec.K256.Field52.Definitions.Lemmas
module L1 = Hacl.Spec.K256.Field52.Lemmas1
module L2 = Hacl.Spec.K256.Field52.Lemmas2
module L3 = Hacl.Spec.K256.Field52.Lemmas3

#set-options "--z3rlimit 100 --fuel 0 --ifuel 0"

let load_felem5_lemma s =
  L1.load_felem5_lemma s
val store_felem5_lemma: f:felem5 -> Lemma
  (requires felem_fits5 f (1,1,1,1,1))
  (ensures  as_nat4 (store_felem5 f) == as_nat5 f)
f: Hacl.Spec.K256.Field52.Definitions.felem5
  -> FStar.Pervasives.Lemma
      (requires Hacl.Spec.K256.Field52.Definitions.felem_fits5 f (1, 1, 1, 1, 1))
      (ensures
        Hacl.Spec.K256.Field52.Definitions.as_nat4 (Hacl.Spec.K256.Field52.store_felem5 f) ==
        Hacl.Spec.K256.Field52.Definitions.as_nat5 f)