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_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)
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
Hacl.Spec.K256.Field52.Definitions.felem5 Lib.IntTypes.uint64 Prims._assert Prims.b2t Prims.op_Equality Prims.int Prims.op_Modulus Hacl.Spec.K256.Field52.Definitions.as_nat5 Lib.IntTypes.v Lib.IntTypes.U64 Lib.IntTypes.SEC Prims.unit Hacl.Spec.K256.MathLemmas.lemma_a_plus_b_pow2_mod2 Prims.op_Addition FStar.Mul.op_Star Hacl.Spec.K256.Field52.Definitions.pow52 Hacl.Spec.K256.Field52.Definitions.pow104 Hacl.Spec.K256.Field52.Definitions.pow156 Hacl.Spec.K256.Field52.Definitions.pow208
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 ->
val lemma_as_nat_mod2: x:felem5 ->
  Lemma (let (x0,x1,x2,x3,x4) = x in as_nat5 x % 2 = v x0 % 2)
x: Hacl.Spec.K256.Field52.Definitions.felem5
  -> FStar.Pervasives.Lemma
    (ensures
      (let _ = x in
        (let FStar.Pervasives.Native.Mktuple5 #_ #_ #_ #_ #_ x0 _ _ _ _ = _ in
          Hacl.Spec.K256.Field52.Definitions.as_nat5 x % 2 = Lib.IntTypes.v x0 % 2)
        <:
        Type0))