val lemma_nat_from_bytes_be_mod2: f:LSeq.lseq uint8 32 ->
  Lemma (BSeq.nat_from_bytes_be f % 2 = v (LSeq.index f 31) % 2)
let lemma_nat_from_bytes_be_mod2 f =
  let x0 = LSeq.index f 31 in
  BSeq.nat_from_intseq_be_slice_lemma f 31;
  BSeq.nat_from_intseq_be_lemma0 (LSeq.slice f 31 32);
  assert (BSeq.nat_from_intseq_be f == v x0 + pow2 8 * BSeq.nat_from_intseq_be (LSeq.slice f 0 31));
  ML.lemma_a_plus_b_pow2_mod2 (v x0) (BSeq.nat_from_intseq_be (LSeq.slice f 0 31)) 8
val lemma_nat_from_bytes_be_mod2: f:LSeq.lseq uint8 32 ->
  Lemma (BSeq.nat_from_bytes_be f % 2 = v (LSeq.index f 31) % 2)
let lemma_nat_from_bytes_be_mod2 f =
let x0 = LSeq.index f 31 in
BSeq.nat_from_intseq_be_slice_lemma f 31;
BSeq.nat_from_intseq_be_lemma0 (LSeq.slice f 31 32);
assert (BSeq.nat_from_intseq_be f == v x0 + pow2 8 * BSeq.nat_from_intseq_be (LSeq.slice f 0 31));
ML.lemma_a_plus_b_pow2_mod2 (v x0) (BSeq.nat_from_intseq_be (LSeq.slice f 0 31)) 8
Hacl.Spec.K256.Field52.Definitions.Lemmas.fst.checked
Spec.K256.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Hacl.Spec.K256.MathLemmas.fst.checked Hacl.Spec.K256.Field52.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Seq.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.Definitions.Lemmas.fst
Lib.Sequence.lseq Lib.IntTypes.uint8 Hacl.Spec.K256.MathLemmas.lemma_a_plus_b_pow2_mod2 Lib.IntTypes.v Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.ByteSequence.nat_from_intseq_be Lib.Sequence.slice Prims.unit Prims._assert Prims.eq2 Prims.int Prims.op_Addition FStar.Mul.op_Star Prims.pow2 Lib.ByteSequence.nat_from_intseq_be_lemma0 Lib.ByteSequence.nat_from_intseq_be_slice_lemma Lib.IntTypes.int_t FStar.Seq.Base.index Lib.Sequence.to_seq Lib.Sequence.index
module Hacl.Spec.K256.Field52.Definitions.Lemmas

open FStar.Mul
open Lib.IntTypes

open Hacl.Spec.K256.Field52.Definitions

module LSeq = Lib.Sequence
module BSeq = Lib.ByteSequence

module S = Spec.K256
module ML = Hacl.Spec.K256.MathLemmas

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

val lemma_as_nat_mod2: x:felem5 ->
  Lemma (let (x0,x1,x2,x3,x4) = x in as_nat5 x % 2 = v x0 % 2)
let lemma_as_nat_mod2 x =
  let (x0,x1,x2,x3,x4) = x in
  assert (as_nat5 x = v x0 + v x1 * pow52 + v x2 * pow104 + v x3 * pow156 + v x4 * pow208);
  assert (as_nat5 x % 2 = (v x0 + v x1 * pow52 + v x2 * pow104 + v x3 * pow156 + v x4 * pow208) % 2);
  ML.lemma_a_plus_b_pow2_mod2 (v x0 + v x1 * pow52 + v x2 * pow104 + v x3 * pow156) (v x4) 208;
  ML.lemma_a_plus_b_pow2_mod2 (v x0 + v x1 * pow52 + v x2 * pow104) (v x3) 156;
  ML.lemma_a_plus_b_pow2_mod2 (v x0 + v x1 * pow52) (v x2) 104;
  ML.lemma_a_plus_b_pow2_mod2 (v x0) (v x1) 52;
  assert (as_nat5 x % 2 = v x0 % 2)


val lemma_nat_from_bytes_be_mod2: f:LSeq.lseq uint8 32 ->
  Lemma (BSeq.nat_from_bytes_be f % 2 = v (LSeq.index f 31) % 2)
val lemma_nat_from_bytes_be_mod2: f:LSeq.lseq uint8 32 ->
  Lemma (BSeq.nat_from_bytes_be f % 2 = v (LSeq.index f 31) % 2)
f: Lib.Sequence.lseq Lib.IntTypes.uint8 32
  -> FStar.Pervasives.Lemma
    (ensures Lib.ByteSequence.nat_from_bytes_be f % 2 = Lib.IntTypes.v (Lib.Sequence.index f 31) % 2
    )