val 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)
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);
  ()
val 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)
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);
()
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
Prims.nat Prims.b2t Prims.op_GreaterThan Vale.Def.Words_s.natN Prims.pow2 Prims.unit Prims._assert Prims.op_Equality Prims.int FStar.Mul.op_Star Prims.op_Subtraction Prims.op_Addition FStar.Math.Lemmas.pow2_plus Vale.Curve25519.Fast_lemmas_internal.lemma_mul_bounds_le Prims.l_True Prims.squash Prims.l_and Prims.op_LessThan Prims.op_LessThanOrEqual 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)
val 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)

    b: Prims.nat{b > 1} ->
    x: Vale.Def.Words_s.natN (Prims.pow2 b) ->
    y: Vale.Def.Words_s.natN (Prims.pow2 b)
  -> FStar.Pervasives.Lemma
    (ensures x * y < Prims.pow2 (2 * b) - 1 /\ x * y <= Prims.pow2 (2 * b) - 2 * Prims.pow2 b + 1)