val load_felem5_lemma: s:felem4 ->
  Lemma (let f = load_felem5 s in
    felem_fits5 f (1,1,1,1,1) /\ as_nat5 f == as_nat4 s)
let load_felem5_lemma s =
  L1.load_felem5_lemma s
val load_felem5_lemma: s:felem4 ->
  Lemma (let f = load_felem5 s in
    felem_fits5 f (1,1,1,1,1) /\ as_nat5 f == as_nat4 s)
let load_felem5_lemma s =
L1.load_felem5_lemma s
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.felem4 Hacl.Spec.K256.Field52.Lemmas1.load_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"
val load_felem5_lemma: s:felem4 ->
  Lemma (let f = load_felem5 s in
    felem_fits5 f (1,1,1,1,1) /\ as_nat5 f == as_nat4 s)
s: Hacl.Spec.K256.Field52.Definitions.felem4
  -> FStar.Pervasives.Lemma
    (ensures
      (let f = Hacl.Spec.K256.Field52.load_felem5 s in
        Hacl.Spec.K256.Field52.Definitions.felem_fits5 f (1, 1, 1, 1, 1) /\
        Hacl.Spec.K256.Field52.Definitions.as_nat5 f == Hacl.Spec.K256.Field52.Definitions.as_nat4 s
      ))