val lemma_mod_add_distr (a:int) (b:int) (n:pos) : Lemma ((a + b % n) % n = (a + b) % n)
let lemma_mod_add_distr (a:int) (b:int) (n:pos) =
  lemma_div_mod b n;
  // (a + b) % n == (a + (b % n) + (b / n) * n) % n
  lemma_mod_plus (a + (b % n)) (b / n) n
val lemma_mod_add_distr (a:int) (b:int) (n:pos) : Lemma ((a + b % n) % n = (a + b) % n)
let lemma_mod_add_distr (a b: int) (n: pos) =
lemma_div_mod b n;
lemma_mod_plus (a + (b % n)) (b / n) 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.int Prims.pos Vale.Math.Lemmas.Int.lemma_mod_plus Prims.op_Addition Prims.op_Modulus Prims.op_Division Prims.unit Vale.Math.Lemmas.Int.lemma_div_mod
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"

let lt_multiple_is_equal (a:nat) (b:nat) (x:int) (n:pos) =
  assert (0 * n == 0);
  bounded_multiple_is_zero x n

let add_div_mod_1 (a:int) (n:pos) : Lemma ((a + n) % n == a % n /\ (a + n) / n == a / n + 1) =
  lemma_div_mod a n;
  lemma_div_mod (a + n) n;
  // ((a + n) % n) == a % n + (a / n) * n + n - ((a + n) / n) * n
  FStar.Math.Lemmas.distributivity_add_left (a / n) 1 n;
  FStar.Math.Lemmas.distributivity_sub_left (a / n + 1) ((a + n) / n) n;
  // (((a + n) % n) == a % n + (a / n + 1 - (a + n) / n) * n
  lt_multiple_is_equal ((a + n) % n) (a % n) (a / n + 1 - (a + n) / n) n;
  ()

let sub_div_mod_1 (a:int) (n:pos) : Lemma ((a - n) % n == a % n /\ (a - n) / n == a / n - 1) =
  lemma_div_mod a n;
  lemma_div_mod (a - n) n;
  // ((a - n) % n) == a % n - n + (a / n) * n - ((a - n) / n) * n
  FStar.Math.Lemmas.distributivity_add_left (a / n) 1 n;
  FStar.Math.Lemmas.distributivity_sub_left (a / n - 1) ((a - n) / n) n;
  // ((a - n) % n) == a % n + (a / n - 1 - (a - n) / n) * n
  lt_multiple_is_equal ((a - n) % n) (a % n) (a / n - 1 - (a - n) / n) n;
  ()

let rec lemma_div_mod_plus (a:int) (b:int) (n:pos) : Lemma
  (requires True)
  (ensures
    (a + b * n) / n = a / n + b /\
    (a + b * n) % n = a % n
  )
  (decreases (if b > 0 then b else -b))
  =
  if b = 0 then ()
  else if b > 0 then
  (
    lemma_div_mod_plus a (b - 1) n;
    sub_div_mod_1 (a + b * n) n
  )
  else // b < 0
  (
    lemma_div_mod_plus a (b + 1) n;
    add_div_mod_1 (a + b * n) n
  )

let lemma_div_plus (a:int) (b:int) (n:pos) = lemma_div_mod_plus a b n
let lemma_mod_plus (a:int) (b:int) (n:pos) = lemma_div_mod_plus a b n

let cancel_mul_div (a:int) (n:pos) =
  small_div 0 n;
  lemma_div_plus 0 a n

let cancel_mul_mod (a:int) (n:pos) =
  small_mod 0 n;
  lemma_mod_plus 0 a n

let mod_add_both (a:int) (b:int) (x:int) (n:pos) =
  lemma_div_mod a n;
  lemma_div_mod b n;
  lemma_div_mod (a + x) n;
  lemma_div_mod (b + x) n;
  let xx = (b + x) / n - (a + x) / n - b / n + a / n in
  FStar.Math.Lemmas.distributivity_sub_left ((b + x) / n) ((a + x) / n) n;
  FStar.Math.Lemmas.distributivity_sub_left ((b + x) / n - (a + x) / n) (b / n) n;
  FStar.Math.Lemmas.distributivity_add_left ((b + x) / n - (a + x) / n - b / n) (a / n) n;
  lt_multiple_is_equal ((a + x) % n) ((b + x) % n) xx n
val lemma_mod_add_distr (a:int) (b:int) (n:pos) : Lemma ((a + b % n) % n = (a + b) % n)
a: Prims.int -> b: Prims.int -> n: Prims.pos
  -> FStar.Pervasives.Lemma (ensures (a + b % n) % n = (a + b) % n)