val lemma_mul_pow256_add (x y: nat) : Lemma ((x + y * pow2_256) % prime == (x + y * 38) % prime)
let lemma_mul_pow256_add (x y:nat) :
  Lemma ((x + y * pow2_256) % prime == (x + y * 38) % prime)
  =
  assert_norm (pow2_256 % prime == 38);
  ()
val lemma_mul_pow256_add (x y: nat) : Lemma ((x + y * pow2_256) % prime == (x + y * 38) % prime)
let lemma_mul_pow256_add (x y: nat) : Lemma ((x + y * pow2_256) % prime == (x + y * 38) % prime) =
assert_norm (pow2_256 % prime == 38);
()
Vale.Curve25519.FastHybrid_helpers.fsti.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Curve25519.Fast_defs.fst.checked prims.fst.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Calc.fsti.checked
Vale.Curve25519.FastHybrid_helpers.fsti
Prims.nat Prims.unit FStar.Pervasives.assert_norm Prims.eq2 Prims.int Prims.op_Modulus Vale.Curve25519.Fast_defs.pow2_256 Vale.Curve25519.Fast_defs.prime Prims.l_True Prims.squash Prims.op_Addition FStar.Mul.op_Star Prims.Nil FStar.Pervasives.pattern
module Vale.Curve25519.FastHybrid_helpers

open Vale.Def.Words_s
open Vale.Def.Types_s
open FStar.Mul
open FStar.Tactics
open FStar.Tactics.CanonCommSemiring
open Vale.Curve25519.Fast_defs
open FStar.Calc

let int_canon = fun _ -> norm [delta; zeta; iota]; int_semiring () //; dump "Final"

unfold let pow2_63:nat = 0x8000000000000000

let _ = assert_norm (pow2_63 == pow2 63)

let lemma_mul_pow256_add (x y:nat) :
  Lemma ((x + y * pow2_256) % prime == (x + y * 38) % prime)
val lemma_mul_pow256_add (x y: nat) : Lemma ((x + y * pow2_256) % prime == (x + y * 38) % prime)
x: Prims.nat -> y: Prims.nat
  -> FStar.Pervasives.Lemma
    (ensures
      (x + y * Vale.Curve25519.Fast_defs.pow2_256) % Vale.Curve25519.Fast_defs.prime ==
      (x + y * 38) % Vale.Curve25519.Fast_defs.prime)