val fmul15_lemma: m1:scale64_5 -> m2:nat -> f:felem5 -> c:uint64 -> Lemma
  (requires felem_fits5 f m1 /\ v c <= m2 /\ m1 ** mk_nat5 m2 <=* (4096,4096,4096,4096,65536))
  (ensures (let r = mul15 f c in
    feval5 r == v c * feval5 f % S.prime /\ felem_fits5 r (m1 ** mk_nat5 m2)))
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
val fmul15_lemma: m1:scale64_5 -> m2:nat -> f:felem5 -> c:uint64 -> Lemma
  (requires felem_fits5 f m1 /\ v c <= m2 /\ m1 ** mk_nat5 m2 <=* (4096,4096,4096,4096,65536))
  (ensures (let r = mul15 f c in
    feval5 r == v c * feval5 f % S.prime /\ felem_fits5 r (m1 ** mk_nat5 m2)))
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
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.scale64_5 Prims.nat Hacl.Spec.K256.Field52.Definitions.felem5 Lib.IntTypes.uint64 FStar.Math.Lemmas.lemma_mod_mul_distr_r Lib.IntTypes.v Lib.IntTypes.U64 Lib.IntTypes.SEC Hacl.Spec.K256.Field52.Definitions.as_nat5 Spec.K256.PointOps.prime Prims.unit Prims._assert Prims.eq2 Prims.int FStar.Mul.op_Star Hacl.Spec.K256.Field52.Lemmas.mul15_lemma Hacl.Spec.K256.Field52.mul15
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
val fmul15_lemma: m1:scale64_5 -> m2:nat -> f:felem5 -> c:uint64 -> Lemma
  (requires felem_fits5 f m1 /\ v c <= m2 /\ m1 ** mk_nat5 m2 <=* (4096,4096,4096,4096,65536))
  (ensures (let r = mul15 f c in
    feval5 r == v c * feval5 f % S.prime /\ felem_fits5 r (m1 ** mk_nat5 m2)))

    m1: Hacl.Spec.K256.Field52.Definitions.scale64_5 ->
    m2: Prims.nat ->
    f: Hacl.Spec.K256.Field52.Definitions.felem5 ->
    c: Lib.IntTypes.uint64
  -> FStar.Pervasives.Lemma
      (requires
        Hacl.Spec.K256.Field52.Definitions.felem_fits5 f m1 /\ Lib.IntTypes.v c <= m2 /\
        m1 ** Hacl.Spec.K256.Field52.Definitions.mk_nat5 m2 <=*
        FStar.Pervasives.Native.Mktuple5 4096 4096 4096 4096 65536)
      (ensures
        (let r = Hacl.Spec.K256.Field52.mul15 f c in
          Hacl.Spec.K256.Field52.Definitions.feval5 r ==
          Lib.IntTypes.v c * Hacl.Spec.K256.Field52.Definitions.feval5 f % Spec.K256.PointOps.prime /\
          Hacl.Spec.K256.Field52.Definitions.felem_fits5 r
            (m1 ** Hacl.Spec.K256.Field52.Definitions.mk_nat5 m2)))