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.FastMul_helpers.fst.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Curve25519.Fast_lemmas_internal.fsti.checked Vale.Curve25519.Fast_defs.fst.checked prims.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Vale.Curve25519.FastMul_helpers.fst
Prims.nat Prims.b2t Prims.op_GreaterThan Vale.Def.Words_s.natN Prims.pow2 Prims._assert Prims.op_Equality Prims.int FStar.Mul.op_Star Prims.op_Subtraction Prims.op_Addition Prims.unit 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.FastMul_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 Vale.Curve25519.Fast_lemmas_internal
open FStar.Math.Lemmas
#reset-options "--using_facts_from '* -FStar.Tactics -FStar.Reflection'"

#push-options "--z3rlimit 10"
let lemma_mul_pow2_bound (b:nat{b > 1}) (x y:natN (pow2 b))
  : Lemma (x * y < pow2 (2*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)