val lemma_mul_nat_bound (a a' b b':nat) : Lemma
  (requires a <= a' /\ b <= b')
  (ensures 0 <= a * b /\ a * b <= a' * b')
let lemma_mul_nat_bound a a' b b' =
  let open FStar.Math.Lemmas in
  nat_times_nat_is_nat a b;
  lemma_mult_le_left a b b'; // a * b <= a * b'
  lemma_mult_le_right b' a a'; // a * b' <= a' * b'
  ()
val lemma_mul_nat_bound (a a' b b':nat) : Lemma
  (requires a <= a' /\ b <= b')
  (ensures 0 <= a * b /\ a * b <= a' * b')
let lemma_mul_nat_bound a a' b b' =
let open FStar.Math.Lemmas in
nat_times_nat_is_nat a b;
lemma_mult_le_left a b b';
lemma_mult_le_right b' a a';
()
Vale.Bignum.Defs.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Vale.Bignum.Defs.fst
Prims.nat Prims.unit FStar.Math.Lemmas.lemma_mult_le_right FStar.Math.Lemmas.lemma_mult_le_left FStar.Math.Lemmas.nat_times_nat_is_nat
module Vale.Bignum.Defs
open FStar.Mul
val lemma_mul_nat_bound (a a' b b':nat) : Lemma
  (requires a <= a' /\ b <= b')
  (ensures 0 <= a * b /\ a * b <= a' * b')
a: Prims.nat -> a': Prims.nat -> b: Prims.nat -> b': Prims.nat
  -> FStar.Pervasives.Lemma (requires a <= a' /\ b <= b') (ensures 0 <= a * b /\ a * b <= a' * b')