val lt_multiple_is_equal (a:nat) (b:nat) (x:int) (n:pos) : Lemma
  (requires a < n /\ b < n /\ a == b + x * n)
  (ensures a == b /\ x == 0)
let lt_multiple_is_equal (a:nat) (b:nat) (x:int) (n:pos) =
  assert (0 * n == 0);
  bounded_multiple_is_zero x n
val lt_multiple_is_equal (a:nat) (b:nat) (x:int) (n:pos) : Lemma
  (requires a < n /\ b < n /\ a == b + x * n)
  (ensures a == b /\ x == 0)
let lt_multiple_is_equal (a b: nat) (x: int) (n: pos) =
assert (0 * n == 0);
bounded_multiple_is_zero x n
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.nat Prims.int Prims.pos Vale.Math.Lemmas.Int.bounded_multiple_is_zero Prims.unit Prims._assert Prims.eq2 FStar.Mul.op_Star
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) = ()

let lemma_div_lt a n m =
  if a >= 0 then FStar.Math.Lemmas.lemma_div_lt a n m
  else ()

let bounded_multiple_is_zero (x:int) (n:pos) = ()

let small_div (a:nat) (n:pos) : Lemma (requires a < n) (ensures a / n == 0) = ()
let small_mod (a:nat) (n:pos) : Lemma (requires a < n) (ensures a % n == a) = ()

#reset-options "--initial_fuel 0 --max_fuel 0 --z3cliopt smt.arith.nl=false --smtencoding.elim_box true --smtencoding.l_arith_repr native --smtencoding.nl_arith_repr wrapped"
val lt_multiple_is_equal (a:nat) (b:nat) (x:int) (n:pos) : Lemma
  (requires a < n /\ b < n /\ a == b + x * n)
  (ensures a == b /\ x == 0)
a: Prims.nat -> b: Prims.nat -> x: Prims.int -> n: Prims.pos
  -> FStar.Pervasives.Lemma (requires a < n /\ b < n /\ a == b + x * n) (ensures a == b /\ x == 0)