val load_felem5_lemma_fits: s:felem4 -> f:felem5 -> Lemma
  (requires
   (let (s0,s1,s2,s3) = s in
    let (f0,f1,f2,f3,f4) = f in
    v f0 == v s0 % pow2 52 /\
    v f1 == v s0 / pow2 52 + v s1 % pow2 40 * pow2 12 /\
    v f2 = v s1 / pow2 40 + v s2 % pow2 28 * pow2 24 /\
    v f3 = v s2 / pow2 28 + v s3 % pow2 16 * pow2 36 /\
    v f4 = v s3 / pow2 16))
  (ensures felem_fits5 f (1,1,1,1,1))
let load_felem5_lemma_fits s f =
  let (s0,s1,s2,s3) = s in
  let (f0,f1,f2,f3,f4) = f in
  assert (v f0 < pow2 52);

  Math.Lemmas.lemma_div_lt (v s0) 64 52;
  ML.lemma_a_div_b_plus_c_mod_d_mul_e (v s0) 52 (v s1) 40 12;
  assert (v f1 < pow2 52);

  Math.Lemmas.lemma_div_lt (v s1) 64 40;
  ML.lemma_a_div_b_plus_c_mod_d_mul_e (v s1) 40 (v s2) 28 24;
  assert (v f2 < pow2 52);

  Math.Lemmas.lemma_div_lt (v s2) 64 28;
  ML.lemma_a_div_b_plus_c_mod_d_mul_e (v s2) 28 (v s3) 16 36;
  assert (v f3 < pow2 52);

  assert (v f4 = v s3 / pow2 16);
  Math.Lemmas.lemma_div_lt (v s3) 64 16;
  assert (v f4 < pow2 48)
val load_felem5_lemma_fits: s:felem4 -> f:felem5 -> Lemma
  (requires
   (let (s0,s1,s2,s3) = s in
    let (f0,f1,f2,f3,f4) = f in
    v f0 == v s0 % pow2 52 /\
    v f1 == v s0 / pow2 52 + v s1 % pow2 40 * pow2 12 /\
    v f2 = v s1 / pow2 40 + v s2 % pow2 28 * pow2 24 /\
    v f3 = v s2 / pow2 28 + v s3 % pow2 16 * pow2 36 /\
    v f4 = v s3 / pow2 16))
  (ensures felem_fits5 f (1,1,1,1,1))
let load_felem5_lemma_fits s f =
let s0, s1, s2, s3 = s in
let f0, f1, f2, f3, f4 = f in
assert (v f0 < pow2 52);
Math.Lemmas.lemma_div_lt (v s0) 64 52;
ML.lemma_a_div_b_plus_c_mod_d_mul_e (v s0) 52 (v s1) 40 12;
assert (v f1 < pow2 52);
Math.Lemmas.lemma_div_lt (v s1) 64 40;
ML.lemma_a_div_b_plus_c_mod_d_mul_e (v s1) 40 (v s2) 28 24;
assert (v f2 < pow2 52);
Math.Lemmas.lemma_div_lt (v s2) 64 28;
ML.lemma_a_div_b_plus_c_mod_d_mul_e (v s2) 28 (v s3) 16 36;
assert (v f3 < pow2 52);
assert (v f4 = v s3 / pow2 16);
Math.Lemmas.lemma_div_lt (v s3) 64 16;
assert (v f4 < pow2 48)
Hacl.Spec.K256.Field52.Lemmas1.fst.checked
Spec.K256.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Hacl.Spec.K256.MathLemmas.fst.checked Hacl.Spec.K256.Field52.Definitions.fst.checked Hacl.Spec.K256.Field52.fst.checked FStar.UInt32.fsti.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.Lemmas1.fst
Hacl.Spec.K256.Field52.Definitions.felem4 Hacl.Spec.K256.Field52.Definitions.felem5 Lib.IntTypes.uint64 Prims._assert Prims.b2t Prims.op_LessThan Lib.IntTypes.v Lib.IntTypes.U64 Lib.IntTypes.SEC Prims.pow2 Prims.unit FStar.Math.Lemmas.lemma_div_lt Prims.op_Equality Prims.int Prims.op_Division Hacl.Spec.K256.MathLemmas.lemma_a_div_b_plus_c_mod_d_mul_e
module Hacl.Spec.K256.Field52.Lemmas1

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

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

///  Load and store functions

val load_felem5_lemma_as_nat: s:felem4 -> f:felem5 -> Lemma
  (requires
   (let (s0,s1,s2,s3) = s in
    let (f0,f1,f2,f3,f4) = f in
    v f0 == v s0 % pow2 52 /\
    v f1 == v s0 / pow2 52 + v s1 % pow2 40 * pow2 12 /\
    v f2 == v s1 / pow2 40 + v s2 % pow2 28 * pow2 24 /\
    v f3 == v s2 / pow2 28 + v s3 % pow2 16 * pow2 36 /\
    v f4 == v s3 / pow2 16))
  (ensures as_nat5 f == as_nat4 s)

let load_felem5_lemma_as_nat s f =
  let (s0,s1,s2,s3) = s in
  let (f0,f1,f2,f3,f4) = f in
  Math.Lemmas.euclidean_division_definition (v s0) (pow2 52);
  assert_norm (pow2 12 * pow2 52 = pow2 64);
  assert_norm (pow2 52 * pow2 52 = pow2 40 * pow2 64);
  Math.Lemmas.euclidean_division_definition (v s1) (pow2 40);
  assert_norm (pow2 24 * pow2 52 * pow2 52 = pow2 128);
  assert_norm (pow2 52 * pow2 52 * pow2 52 = pow2 28 * pow2 128);
  Math.Lemmas.euclidean_division_definition (v s2) (pow2 25);
  assert_norm (pow2 36 * pow2 52 * pow2 52 * pow2 52 = pow2 192);
  assert_norm (pow2 52 * pow2 52 * pow2 52 * pow2 52 = pow2 16 * pow2 192);
  Math.Lemmas.euclidean_division_definition (v s3) (pow2 16);
  assert (as_nat5 f == v s0 + v s1 * pow2 64 + v s2 * pow2 128 + v s3 * pow2 192)


val load_felem5_lemma_fits: s:felem4 -> f:felem5 -> Lemma
  (requires
   (let (s0,s1,s2,s3) = s in
    let (f0,f1,f2,f3,f4) = f in
    v f0 == v s0 % pow2 52 /\
    v f1 == v s0 / pow2 52 + v s1 % pow2 40 * pow2 12 /\
    v f2 = v s1 / pow2 40 + v s2 % pow2 28 * pow2 24 /\
    v f3 = v s2 / pow2 28 + v s3 % pow2 16 * pow2 36 /\
    v f4 = v s3 / pow2 16))
  (ensures felem_fits5 f (1,1,1,1,1))
val load_felem5_lemma_fits: s:felem4 -> f:felem5 -> Lemma
  (requires
   (let (s0,s1,s2,s3) = s in
    let (f0,f1,f2,f3,f4) = f in
    v f0 == v s0 % pow2 52 /\
    v f1 == v s0 / pow2 52 + v s1 % pow2 40 * pow2 12 /\
    v f2 = v s1 / pow2 40 + v s2 % pow2 28 * pow2 24 /\
    v f3 = v s2 / pow2 28 + v s3 % pow2 16 * pow2 36 /\
    v f4 = v s3 / pow2 16))
  (ensures felem_fits5 f (1,1,1,1,1))
s: Hacl.Spec.K256.Field52.Definitions.felem4 -> f: Hacl.Spec.K256.Field52.Definitions.felem5
  -> FStar.Pervasives.Lemma
      (requires
        (let _ = s in
          (let FStar.Pervasives.Native.Mktuple4 #_ #_ #_ #_ s0 s1 s2 s3 = _ in
            let _ = f in
            (let FStar.Pervasives.Native.Mktuple5 #_ #_ #_ #_ #_ f0 f1 f2 f3 f4 = _ in
              Lib.IntTypes.v f0 == Lib.IntTypes.v s0 % Prims.pow2 52 /\
              Lib.IntTypes.v f1 ==
              Lib.IntTypes.v s0 / Prims.pow2 52 +
              (Lib.IntTypes.v s1 % Prims.pow2 40) * Prims.pow2 12 /\
              Lib.IntTypes.v f2 =
              Lib.IntTypes.v s1 / Prims.pow2 40 +
              (Lib.IntTypes.v s2 % Prims.pow2 28) * Prims.pow2 24 /\
              Lib.IntTypes.v f3 =
              Lib.IntTypes.v s2 / Prims.pow2 28 +
              (Lib.IntTypes.v s3 % Prims.pow2 16) * Prims.pow2 36 /\
              Lib.IntTypes.v f4 = Lib.IntTypes.v s3 / Prims.pow2 16)
            <:
            Type0)
          <:
          Type0)) (ensures Hacl.Spec.K256.Field52.Definitions.felem_fits5 f (1, 1, 1, 1, 1))