val lemma_mul_div_n_lt (#n:nat) (a b:natN n) : Lemma ((a * b) / n < (if n <= 1 then n else n - 1))
let lemma_mul_div_n_lt #n a b =
  let open FStar.Math.Lemmas in
  lemma_mul_n_bound a b;
  lemma_div_le (a * b) ((n - 1) * (n - 1)) n;
  calc (==) {
    (n - 1) * (n - 1);
    == {distributivity_sub_right (n - 1) n 1}
    (n - 1) * n - (n - 1) * 1;
    == {}
    (n - 2) * n + 1;
  };
  if n > 1 then small_division_lemma_1 1 n; // 1 / n == 0
  lemma_div_plus 1 (n - 2) n; // (1 + (n - 2) * n) / n == 1 / n + (n - 2)
  ()
val lemma_mul_div_n_lt (#n:nat) (a b:natN n) : Lemma ((a * b) / n < (if n <= 1 then n else n - 1))
let lemma_mul_div_n_lt #n a b =
let open FStar.Math.Lemmas in
lemma_mul_n_bound a b;
lemma_div_le (a * b) ((n - 1) * (n - 1)) n;
calc ( == ) {
  (n - 1) * (n - 1);
  ( == ) { distributivity_sub_right (n - 1) n 1 }
  (n - 1) * n - (n - 1) * 1;
  ( == ) { () }
  (n - 2) * n + 1;
};
if n > 1 then small_division_lemma_1 1 n;
lemma_div_plus 1 (n - 2) n;
()
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 Prims.unit FStar.Math.Lemmas.lemma_div_plus Prims.op_Subtraction Prims.op_GreaterThan FStar.Math.Lemmas.small_division_lemma_1 Prims.bool FStar.Calc.calc_finish Prims.int Prims.eq2 FStar.Mul.op_Star Prims.op_Addition Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step FStar.Calc.calc_init FStar.Calc.calc_pack FStar.Math.Lemmas.distributivity_sub_right Prims.squash FStar.Math.Lemmas.lemma_div_le Vale.Bignum.Defs.lemma_mul_n_bound
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'
  ()

let lemma_mul_n_bound #n a b =
  lemma_mul_nat_bound a (n - 1) b (n - 1)

#restart-solver
val lemma_mul_div_n_lt (#n:nat) (a b:natN n) : Lemma ((a * b) / n < (if n <= 1 then n else n - 1))
a: Vale.Def.Words_s.natN n -> b: Vale.Def.Words_s.natN n
  -> FStar.Pervasives.Lemma
    (ensures
      a * b / n <
      (match n <= 1 with
        | true -> n
        | _ -> n - 1))