val 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)
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;
  ()
val 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)
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;
()
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.unit FStar.Math.Lemmas.lemma_mult_le_right Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.squash FStar.Mul.op_Star 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)
val 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)
x: Prims.nat -> b_x: Prims.nat -> y: Prims.nat -> b_y: Prims.nat
  -> FStar.Pervasives.Lemma (requires x <= b_x /\ y <= b_y) (ensures x * y <= b_x * b_y)