val lemma_mul_bound64 (x y:nat64) :
  Lemma (x * y < pow2_128 - 1 /\ x * y <= pow2_128 - 2*pow2_64 + 1)
let lemma_mul_bound64 (x y:nat64) :
  Lemma (x * y < pow2_128 - 1 /\ x * y <= pow2_128 - 2*pow2_64 + 1)
 =
 assert_norm (pow2 64 == pow2_64);
 assert_norm (pow2 128 == pow2_128);
 lemma_mul_pow2_bound 64 x y;
 ()
val lemma_mul_bound64 (x y:nat64) :
  Lemma (x * y < pow2_128 - 1 /\ x * y <= pow2_128 - 2*pow2_64 + 1)
let lemma_mul_bound64 (x y: nat64)
    : Lemma (x * y < pow2_128 - 1 /\ x * y <= pow2_128 - 2 * pow2_64 + 1) =
assert_norm (pow2 64 == pow2_64);
assert_norm (pow2 128 == pow2_128);
lemma_mul_pow2_bound 64 x y;
()
Vale.Curve25519.Fast_lemmas_internal.fst.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
Vale.Curve25519.Fast_lemmas_internal.fst
Vale.Def.Types_s.nat64 Prims.unit Vale.Curve25519.Fast_lemmas_internal.lemma_mul_pow2_bound FStar.Pervasives.assert_norm Prims.eq2 Prims.int Prims.pow2 Vale.Def.Words_s.pow2_128 Vale.Def.Words_s.pow2_64 Prims.l_True Prims.squash Prims.l_and Prims.b2t Prims.op_LessThan FStar.Mul.op_Star Prims.op_Subtraction Prims.op_LessThanOrEqual Prims.op_Addition Prims.Nil FStar.Pervasives.pattern
module Vale.Curve25519.Fast_lemmas_internal

open Vale.Def.Words_s
open Vale.Def.Types_s
open FStar.Mul
open FStar.Math.Lemmas

let lemma_mul_bounds_le (x b_x y b_y:nat) : Lemma
  (requires x <= b_x /\ y <= b_y)
  (ensures x * y <= b_x * b_y)
  =
  lemma_mult_le_right b_x y b_y;
  lemma_mult_le_right y x b_x;
  ()

let lemma_mul_pow2_bound (b:nat{b > 1}) (x y:natN (pow2 b)) :
  Lemma (x * y < pow2 (2*b) - 1 /\
         x * y <= pow2 (2*b) - 2*pow2(b) + 1)
  =
  lemma_mul_bounds_le x (pow2 b - 1) y (pow2 b -1);
  pow2_plus b b;
  assert ( (pow2 b - 1) * (pow2 b -1) = pow2 (2*b) - 2*pow2(b) + 1);
  ()

let lemma_mul_bound64 (x y:nat64) :
  Lemma (x * y < pow2_128 - 1 /\ x * y <= pow2_128 - 2*pow2_64 + 1)
val lemma_mul_bound64 (x y:nat64) :
  Lemma (x * y < pow2_128 - 1 /\ x * y <= pow2_128 - 2*pow2_64 + 1)
x: Vale.Def.Types_s.nat64 -> y: Vale.Def.Types_s.nat64
  -> FStar.Pervasives.Lemma
    (ensures
      x * y < Vale.Def.Words_s.pow2_128 - 1 /\
      x * y <= Vale.Def.Words_s.pow2_128 - 2 * Vale.Def.Words_s.pow2_64 + 1)