val lemma_prod_bounds (dst_hi dst_lo x y:nat64) : Lemma
  (requires pow2_64 * dst_hi + dst_lo == x * y)
  (ensures  dst_hi < pow2_64 - 1 /\
            (dst_hi < pow2_64 - 2 \/ dst_lo <= 1)
  )
let lemma_prod_bounds (dst_hi dst_lo x y:nat64) : Lemma
  (requires pow2_64 * dst_hi + dst_lo == x * y)
  (ensures  dst_hi < pow2_64 - 1 /\
            (dst_hi < pow2_64 - 2 \/ dst_lo <= 1)
  )
  =
  let result = x * y in
  FStar.Math.Lemmas.lemma_div_mod result pow2_64;
  //assert (result = pow2_64 * (result / pow2_64) + result % pow2_64);
  //assert (result % pow2_64 == dst_lo);
  //assert (result / pow2_64 == dst_hi);
  lemma_mul_bound64 x y;
  ()
val lemma_prod_bounds (dst_hi dst_lo x y:nat64) : Lemma
  (requires pow2_64 * dst_hi + dst_lo == x * y)
  (ensures  dst_hi < pow2_64 - 1 /\
            (dst_hi < pow2_64 - 2 \/ dst_lo <= 1)
  )
let lemma_prod_bounds (dst_hi dst_lo x y: nat64)
    : Lemma (requires pow2_64 * dst_hi + dst_lo == x * y)
      (ensures dst_hi < pow2_64 - 1 /\ (dst_hi < pow2_64 - 2 \/ dst_lo <= 1)) =
let result = x * y in
FStar.Math.Lemmas.lemma_div_mod result pow2_64;
lemma_mul_bound64 x y;
()
Vale.Curve25519.Fast_lemmas_external.fst.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Curve25519.Fast_lemmas_internal.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
Vale.Curve25519.Fast_lemmas_external.fst
Vale.Def.Types_s.nat64 Prims.unit Vale.Curve25519.Fast_lemmas_internal.lemma_mul_bound64 FStar.Math.Lemmas.lemma_div_mod Vale.Def.Words_s.pow2_64 Prims.int FStar.Mul.op_Star Prims.eq2 Prims.op_Addition Prims.squash Prims.l_and Prims.b2t Prims.op_LessThan Prims.op_Subtraction Prims.l_or Prims.op_LessThanOrEqual Prims.Nil FStar.Pervasives.pattern
module Vale.Curve25519.Fast_lemmas_external

open Vale.Def.Words_s
open Vale.Def.Types_s
open FStar.Mul
open Vale.Curve25519.Fast_lemmas_internal

let lemma_overflow (dst_hi dst_lo addend:nat64) (old_overflow:bit) : Lemma
  (requires dst_hi < pow2_64 - 1 /\
            (dst_hi < pow2_64 - 2 \/ dst_lo <= 1) /\
            addend < pow2_64 - 1 /\
            (old_overflow = 0 \/ addend < pow2_64 - 2))
  (ensures dst_hi < pow2_64 - 2 \/ dst_lo + addend + old_overflow < pow2_64)
  =
  ()


let lemma_prod_bounds (dst_hi dst_lo x y:nat64) : Lemma
  (requires pow2_64 * dst_hi + dst_lo == x * y)
  (ensures  dst_hi < pow2_64 - 1 /\
            (dst_hi < pow2_64 - 2 \/ dst_lo <= 1)
val lemma_prod_bounds (dst_hi dst_lo x y:nat64) : Lemma
  (requires pow2_64 * dst_hi + dst_lo == x * y)
  (ensures  dst_hi < pow2_64 - 1 /\
            (dst_hi < pow2_64 - 2 \/ dst_lo <= 1)
  )

    dst_hi: Vale.Def.Types_s.nat64 ->
    dst_lo: Vale.Def.Types_s.nat64 ->
    x: Vale.Def.Types_s.nat64 ->
    y: Vale.Def.Types_s.nat64
  -> FStar.Pervasives.Lemma (requires Vale.Def.Words_s.pow2_64 * dst_hi + dst_lo == x * y)
      (ensures
        dst_hi < Vale.Def.Words_s.pow2_64 - 1 /\
        (dst_hi < Vale.Def.Words_s.pow2_64 - 2 \/ dst_lo <= 1))