val is_felem_lt_prime_minus_order_vartime5_lemma: f:felem5 -> Lemma
  (requires felem_fits5 f (1,1,1,1,1))
  (ensures  is_felem_lt_prime_minus_order_vartime5 f == (as_nat5 f < S.prime - S.q))
let is_felem_lt_prime_minus_order_vartime5_lemma f =
  assert_norm (S.prime - S.q =
    0xda1722fc9baee + 0x1950b75fc4402 * pow52 + 0x1455123 * pow104)
val is_felem_lt_prime_minus_order_vartime5_lemma: f:felem5 -> Lemma
  (requires felem_fits5 f (1,1,1,1,1))
  (ensures  is_felem_lt_prime_minus_order_vartime5 f == (as_nat5 f < S.prime - S.q))
let is_felem_lt_prime_minus_order_vartime5_lemma f =
assert_norm (S.prime - S.q = 0xda1722fc9baee + 0x1950b75fc4402 * pow52 + 0x1455123 * pow104)
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 FStar.Pervasives.assert_norm Prims.b2t Prims.op_Equality Prims.int Prims.op_Subtraction Spec.K256.PointOps.prime Spec.K256.PointOps.q Prims.op_Addition FStar.Mul.op_Star Hacl.Spec.K256.Field52.Definitions.pow52 Hacl.Spec.K256.Field52.Definitions.pow104 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


let store_felem5_lemma f =
  L1.store_felem5_lemma f


let add5_lemma m1 m2 f1 f2 =
  L1.add5_lemma m1 m2 f1 f2


let fadd5_lemma m1 m2 f1 f2 =
  let r = add5 f1 f2 in
  add5_lemma m1 m2 f1 f2;
  assert (as_nat5 r == as_nat5 f1 + as_nat5 f2);
  Math.Lemmas.modulo_distributivity (as_nat5 f1) (as_nat5 f2) S.prime


let mul15_lemma m1 m2 f c =
  L1.mul15_lemma m1 m2 f c


let fmul15_lemma m1 m2 f c =
  let r = mul15 f c in
  mul15_lemma m1 m2 f c;
  assert (as_nat5 r == v c * as_nat5 f);
  Math.Lemmas.lemma_mod_mul_distr_r (v c) (as_nat5 f) S.prime


#push-options "--ifuel 1"
let is_felem_zero_vartime5_lemma f = ()


let is_felem_ge_prime_vartime5_lemma f =
  let p =
   (u64 0xffffefffffc2f,
    u64 0xfffffffffffff,
    u64 0xfffffffffffff,
    u64 0xfffffffffffff,
    u64 0xffffffffffff) in
  assert_norm (S.prime = as_nat5 p);
  assert_norm (0xffffefffffc2f <= max52);
  assert_norm (0xfffffffffffff = max52);
  assert_norm (0xffffffffffff = max48);
  assert (felem_fits5 p (1,1,1,1,1));
  //LD.lemma_as_nat_decompose f;
  //LD.lemma_as_nat_decompose p;
  LD.lemma_as_nat_bound f;
  LD.lemma_as_nat_bound p
val is_felem_lt_prime_minus_order_vartime5_lemma: f:felem5 -> Lemma
  (requires felem_fits5 f (1,1,1,1,1))
  (ensures  is_felem_lt_prime_minus_order_vartime5 f == (as_nat5 f < S.prime - S.q))
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.is_felem_lt_prime_minus_order_vartime5 f ==
        (Hacl.Spec.K256.Field52.Definitions.as_nat5 f <
        Spec.K256.PointOps.prime - Spec.K256.PointOps.q))