val lemma_mul_n_bound (#n:nat) (a b:natN n) : Lemma (0 <= a * b /\ a * b <= (n - 1) * (n - 1))
let lemma_mul_n_bound #n a b =
  lemma_mul_nat_bound a (n - 1) b (n - 1)
val lemma_mul_n_bound (#n:nat) (a b:natN n) : Lemma (0 <= a * b /\ a * b <= (n - 1) * (n - 1))
let lemma_mul_n_bound #n a b =
lemma_mul_nat_bound a (n - 1) b (n - 1)
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 Vale.Def.Words_s.natN Vale.Bignum.Defs.lemma_mul_nat_bound Prims.op_Subtraction Prims.unit
module Vale.Bignum.Defs
open FStar.Mul

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_n_bound (#n:nat) (a b:natN n) : Lemma (0 <= a * b /\ a * b <= (n - 1) * (n - 1))
a: Vale.Def.Words_s.natN n -> b: Vale.Def.Words_s.natN n
  -> FStar.Pervasives.Lemma (ensures 0 <= a * b /\ a * b <= (n - 1) * (n - 1))