val lemma_div_lt (a:int) (n:nat) (m:nat) : Lemma
  (requires m <= n /\ a < pow2 n)
        (ensures a / pow2 m < pow2 (n-m))
let lemma_div_lt a n m =
  if a >= 0 then FStar.Math.Lemmas.lemma_div_lt a n m
  else ()
val lemma_div_lt (a:int) (n:nat) (m:nat) : Lemma
  (requires m <= n /\ a < pow2 n)
        (ensures a / pow2 m < pow2 (n-m))
let lemma_div_lt a n m =
if a >= 0 then FStar.Math.Lemmas.lemma_div_lt a n m
Vale.Math.Lemmas.Int.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
Vale.Math.Lemmas.Int.fst
Prims.int Prims.nat Prims.op_GreaterThanOrEqual FStar.Math.Lemmas.lemma_div_lt Prims.bool Prims.unit
module Vale.Math.Lemmas.Int
open FStar.Mul

#reset-options "--initial_fuel 0 --max_fuel 0 --z3cliopt smt.arith.nl=true --smtencoding.elim_box true --smtencoding.l_arith_repr native --smtencoding.nl_arith_repr native"

let multiply_fractions (a:int) (n:pos) = ()
let lemma_div_mod (a:int) (n:pos) = ()
val lemma_div_lt (a:int) (n:nat) (m:nat) : Lemma
  (requires m <= n /\ a < pow2 n)
        (ensures a / pow2 m < pow2 (n-m))
a: Prims.int -> n: Prims.nat -> m: Prims.nat
  -> FStar.Pervasives.Lemma (requires m <= n /\ a < Prims.pow2 n)
      (ensures a / Prims.pow2 m < Prims.pow2 (n - m))