diff --git a/ulib/FStar.Math.Lemmas.fst b/ulib/FStar.Math.Lemmas.fst
index ca1d1c21710..3dc80828f8b 100644
--- a/ulib/FStar.Math.Lemmas.fst
+++ b/ulib/FStar.Math.Lemmas.fst
@@ -21,33 +21,16 @@ open FStar.Math.Lib
 #push-options "--fuel 0 --ifuel 0"
 
 (* Lemma: definition of Euclidean division *)
-val euclidean_div_axiom: a:int -> b:pos -> Lemma
-  (a - b * (a / b) >= 0 /\ a - b * (a / b) < b)
 let euclidean_div_axiom a b = ()
 
-val lemma_eucl_div_bound: a:int -> b:int -> q:int -> Lemma
-  (requires (a < q))
-  (ensures  (a + q * b < q * (b+1)))
 let lemma_eucl_div_bound a b q = ()
 
-val lemma_mult_le_left: a:nat -> b:int -> c:int -> Lemma
-  (requires (b <= c))
-  (ensures  (a * b <= a * c))
 let lemma_mult_le_left a b c = ()
 
-val lemma_mult_le_right: a:nat -> b:int -> c:int -> Lemma
-  (requires (b <= c))
-  (ensures  (b * a <= c * a))
 let lemma_mult_le_right a b c = ()
 
-val lemma_mult_lt_left: a:pos -> b:int -> c:int -> Lemma
-  (requires (b < c))
-  (ensures  (a * b < a * c))
 let lemma_mult_lt_left a b c = ()
 
-val lemma_mult_lt_right: a:pos -> b:int -> c:int -> Lemma
-  (requires (b < c))
-  (ensures  (b * a < c * a))
 let lemma_mult_lt_right a b c = ()
 
 let lemma_mult_lt_sqr (n:nat) (m:nat) (k:nat{n < k && m < k})
@@ -63,20 +46,14 @@ let lemma_mult_lt_sqr (n:nat) (m:nat) (k:nat{n < k && m < k})
   }
 
 (* Lemma: multiplication on integers is commutative *)
-val swap_mul: a:int -> b:int -> Lemma (a * b = b * a)
 let swap_mul a b = ()
 
-val lemma_cancel_mul (a b : int) (n : pos) : Lemma (requires (a * n = b * n)) (ensures (a = b))
 let lemma_cancel_mul a b n = ()
 
 (* Lemma: multiplication is right distributive over addition *)
-val distributivity_add_left: a:int -> b:int -> c:int -> Lemma
-  ((a + b) * c = a * c + b * c)
 let distributivity_add_left a b c = ()
 
 (* Lemma: multiplication is left distributive over addition *)
-val distributivity_add_right: a:int -> b:int -> c:int -> Lemma
-  (a * (b + c) = a * b + a * c)
 let distributivity_add_right a b c =
   calc (==) {
     a * (b + c);
@@ -90,57 +67,34 @@ let distributivity_add_right a b c =
 
 (* Lemma: multiplication is associative, hence parenthesizing is meaningless *)
 (* GM: This is really just an identity since the LHS is associated to the left *)
-val paren_mul_left: a:int -> b:int -> c:int -> Lemma
-  (a * b * c = (a * b) * c)
 let paren_mul_left a b c = ()
 
 (* Lemma: multiplication is associative, hence parenthesizing is meaningless *)
-val paren_mul_right: a:int -> b:int -> c:int -> Lemma
-  (a * b * c = a * (b * c))
 let paren_mul_right a b c = ()
 
 (* Lemma: addition is associative, hence parenthesizing is meaningless *)
-val paren_add_left: a:int -> b:int -> c:int -> Lemma
-  (a + b + c = (a + b) + c)
 let paren_add_left a b c = ()
 
 (* Lemma: addition is associative, hence parenthesizing is meaningless *)
-val paren_add_right: a:int -> b:int -> c:int -> Lemma
-  (a + b + c = a + (b + c))
 let paren_add_right a b c = ()
 
-val addition_is_associative: a:int -> b:int -> c:int -> Lemma
-  (a + b + c = (a + b) + c /\ a + b + c = a + (b + c))
 let addition_is_associative a b c = ()
 
-val subtraction_is_distributive: a:int -> b:int -> c:int -> Lemma
-  (a - b + c = (a - b) + c /\
-   a - b - c = a - (b + c) /\
-   a - b - c = (a - b) - c /\
-   a + (-b - c) = a - b - c /\
-   a - (b - c) = a - b + c)
 let subtraction_is_distributive a b c = ()
 
-val swap_add_plus_minus: a:int -> b:int -> c:int -> Lemma
-  (a + b - c = (a - c) + b)
 let swap_add_plus_minus a b c = ()
 
 (* Lemma: minus applies to the whole term *)
-val neg_mul_left: a:int -> b:int -> Lemma (-(a * b) = (-a) * b)
 let neg_mul_left a b = ()
 
 (* Lemma: minus applies to the whole term *)
-val neg_mul_right: a:int -> b:int -> Lemma (-(a * b) = a * (-b))
 let neg_mul_right a b = ()
 
-val swap_neg_mul: a:int -> b:int -> Lemma ((-a) * b = a * (-b))
 let swap_neg_mul a b =
   neg_mul_left a b;
   neg_mul_right a b
 
 (* Lemma: multiplication is left distributive over subtraction *)
-val distributivity_sub_left: a:int -> b:int -> c:int ->
-  Lemma ((a - b) * c = a * c - b * c)
 let distributivity_sub_left a b c =
   calc (==) {
     (a - b) * c;
@@ -153,8 +107,6 @@ let distributivity_sub_left a b c =
   }
 
 (* Lemma: multiplication is right distributive over subtraction *)
-val distributivity_sub_right: a:int -> b:int -> c:int ->
-  Lemma ((a * (b - c) = a * b - a * c))
 let distributivity_sub_right a b c =
   calc (==) {
     a * (b - c);
@@ -167,21 +119,12 @@ let distributivity_sub_right a b c =
   }
 
 (* Lemma: multiplication precedence on addition *)
-val mul_binds_tighter: a:int -> b:int -> c:int -> Lemma (a + (b * c) = a + b * c)
 let mul_binds_tighter a b c = ()
 
-val lemma_abs_mul : a:int -> b:int -> Lemma (abs a * abs b = abs (a * b))
 let lemma_abs_mul a b = ()
 
-val lemma_abs_bound : a:int -> b:nat -> Lemma (abs a < b <==> -b < a /\ a < b)
 let lemma_abs_bound a b = ()
 
-(* Lemma: multiplication keeps symmetric bounds :
-    b > 0 && d > 0 && -b < a < b && -d < c < d ==> - b * d < a * c < b * d *)
-val mul_ineq1: a:int -> b:nat -> c:int -> d:nat -> Lemma
-    (requires (-b < a /\ a < b /\
-               -d < c /\ c < d))
-    (ensures  (-(b * d) < a * c /\ a * c < b * d))
 let mul_ineq1 a b c d =
   if a = 0 || c = 0 then ()
   else begin
@@ -206,48 +149,31 @@ let mul_one_right_is_same (n : int) : Lemma(n * 1 = n) = ()
 let mul_zero_left_is_zero (n : int) : Lemma(0 * n = 0) = ()
 let mul_zero_right_is_zero (n : int) : Lemma(n * 0 = 0) = ()
 
-val nat_times_nat_is_nat: a:nat -> b:nat -> Lemma (a * b >= 0)
 let nat_times_nat_is_nat a b = ()
 
-val pos_times_pos_is_pos: a:pos -> b:pos -> Lemma (a * b > 0)
 let pos_times_pos_is_pos a b = ()
 
-val nat_over_pos_is_nat: a:nat -> b:pos -> Lemma (a / b >= 0)
 let nat_over_pos_is_nat a b = ()
 
-val nat_plus_nat_equal_zero_lemma: a:nat -> b:nat{a + b = 0} -> Lemma(a = 0 /\ b = 0)
 let nat_plus_nat_equal_zero_lemma a b = ()
 
-val int_times_int_equal_zero_lemma: a:int -> b:int{a * b = 0} -> Lemma(a = 0 \/ b = 0)
 let int_times_int_equal_zero_lemma a b = ()
 
 #push-options "--fuel 1"
-val pow2_double_sum: n:nat -> Lemma (pow2 n + pow2 n = pow2 (n + 1))
 let pow2_double_sum n = ()
 
-val pow2_double_mult: n:nat -> Lemma (2 * pow2 n = pow2 (n + 1))
 let pow2_double_mult n = pow2_double_sum n
 
-val pow2_lt_compat: n:nat -> m:nat -> Lemma
-  (requires (m < n))
-  (ensures  (pow2 m < pow2 n))
-  (decreases m)
 let rec pow2_lt_compat n m =
   match m with
   | 0 -> ()
   | _ -> pow2_lt_compat (n-1) (m-1)
 #pop-options
 
-val pow2_le_compat: n:nat -> m:nat -> Lemma
-  (requires (m <= n))
-  (ensures  (pow2 m <= pow2 n))
 let pow2_le_compat n m =
   if m < n then pow2_lt_compat n m
 
 #push-options "--fuel 1"
-val pow2_plus: n:nat -> m:nat -> Lemma
-  (ensures (pow2 n * pow2 m = pow2 (n + m)))
-  (decreases n)
 let rec pow2_plus n m =
   match n with
   | 0 -> ()
@@ -255,61 +181,40 @@ let rec pow2_plus n m =
 #pop-options
 
 (* Lemma : definition of the exponential property of pow2 *)
-val pow2_minus: n:nat -> m:nat{ n >= m } -> Lemma
-  ((pow2 n) / (pow2 m) = pow2 (n - m))
 let pow2_minus n m =
   pow2_plus (n - m) m;
   slash_star_axiom (pow2 (n - m)) (pow2 m) (pow2 n)
 
 (* Lemma: loss of precision in euclidean division *)
-val multiply_fractions (a:int) (n:nonzero) : Lemma (n * ( a / n ) <= a)
 let multiply_fractions a n = ()
 
 (** Same as `small_mod` *)
-val modulo_lemma: a:nat -> b:pos -> Lemma (requires (a < b)) (ensures (a % b = a))
 let modulo_lemma a b = ()
 
 (** Same as `lemma_div_def` in Math.Lib *)
-val lemma_div_mod: a:int -> p:nonzero -> Lemma (a = p * (a / p) + a % p)
 let lemma_div_mod a p = ()
 
-val lemma_mod_lt: a:int -> p:pos -> Lemma (0 <= a % p /\ a % p < p /\ (a >= 0 ==> a % p <= a))
 let lemma_mod_lt a p = ()
 
-val lemma_div_lt_nat: a:int -> n:nat -> m:nat{m <= n} ->
-  Lemma (requires (a < pow2 n))
-        (ensures  (a / pow2 m < pow2 (n-m)))
 let lemma_div_lt_nat a n m =
   lemma_div_mod a (pow2 m);
   assert(a = pow2 m * (a / pow2 m) + a % pow2 m);
   pow2_plus m (n-m);
   assert(pow2 n = pow2 m * pow2 (n - m))
 
-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 lemma_div_lt_nat a n m
 
-val bounded_multiple_is_zero (x:int) (n:pos) : Lemma
-  (requires -n < x * n /\ x * n < n)
-  (ensures x == 0)
 let bounded_multiple_is_zero (x:int) (n:pos) = ()
 
-val small_div (a:nat) (n:pos) : Lemma (requires a < n) (ensures a / n == 0)
 let small_div (a:nat) (n:pos) : Lemma (requires a < n) (ensures a / n == 0) = ()
 
-val small_mod (a:nat) (n:pos) : Lemma (requires a < n) (ensures a % n == a)
 let small_mod (a:nat) (n:pos) : Lemma (requires a < n) (ensures a % n == a) = ()
 
-val lt_multiple_is_equal (a:nat) (b:nat) (x:int) (n:nonzero) : Lemma
-  (requires a < n /\ b < n /\ a == b + x * n)
-  (ensures a == b /\ x == 0)
 let lt_multiple_is_equal a b x n =
   assert (0 * n == 0);
   bounded_multiple_is_zero x n
 
-val lemma_mod_plus (a:int) (k:int) (n:pos) : Lemma ((a + k * n) % n = a % n)
 let lemma_mod_plus (a:int) (k:int) (n:pos) =
   calc (==) {
     (a+k*n)%n - a%n;
@@ -324,7 +229,6 @@ let lemma_mod_plus (a:int) (k:int) (n:pos) =
   lt_multiple_is_equal ((a+k*n)%n) (a%n) (k + a/n - (a+k*n)/n) n;
   ()
 
-val lemma_div_plus (a:int) (k:int) (n:pos) : Lemma ((a + k * n) / n = a / n + k)
 let lemma_div_plus (a:int) (k:int) (n:pos) =
   calc (==) {
     n * ((a+k*n)/n - a/n);
@@ -344,29 +248,24 @@ let lemma_div_mod_plus (a:int) (k:int) (n:pos) : Lemma ((a + k * n) / n = a / n
     lemma_div_plus a k n;
     lemma_mod_plus a k n
 
-val add_div_mod_1 (a:int) (n:pos) : Lemma ((a + n) % n == a % n /\ (a + n) / n == a / n + 1)
 let add_div_mod_1 a n =
     lemma_mod_plus a 1 n;
     lemma_div_plus a 1 n
 
-val sub_div_mod_1 (a:int) (n:pos) : Lemma ((a - n) % n == a % n /\ (a - n) / n == a / n - 1)
 let sub_div_mod_1 a n =
     lemma_mod_plus a (-1) n;
     lemma_div_plus a (-1) n
 
 #push-options "--smtencoding.elim_box true --smtencoding.nl_arith_repr native"
 
-val cancel_mul_div (a:int) (n:nonzero) : Lemma ((a * n) / n == a)
 let cancel_mul_div (a:int) (n:nonzero) = ()
 
 #pop-options
 
-val cancel_mul_mod (a:int) (n:pos) : Lemma ((a * n) % n == 0)
 let cancel_mul_mod (a:int) (n:pos) =
   small_mod 0 n;
   lemma_mod_plus 0 a 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:int) (b:int) (n:pos) =
   calc (==) {
     (a + b%n) % n;
@@ -376,7 +275,6 @@ let lemma_mod_add_distr (a:int) (b:int) (n:pos) =
     (a + b) % n;
   }
 
-val lemma_mod_sub_distr (a:int) (b:int) (n:pos) : Lemma ((a - b % n) % n = (a - b) % n)
 let lemma_mod_sub_distr (a:int) (b:int) (n:pos) =
   calc (==) {
     (a - b%n) % n;
@@ -388,10 +286,8 @@ let lemma_mod_sub_distr (a:int) (b:int) (n:pos) =
     (a - b) % n;
   }
 
-val lemma_mod_sub_0: a:pos -> Lemma ((-1) % a = a - 1)
 let lemma_mod_sub_0 a = ()
 
-val lemma_mod_sub_1: a:pos -> b:pos{a < b} -> Lemma ((-a) % b = b - (a%b))
 let lemma_mod_sub_1 a b =
   calc (==) {
     (-a) % b;
@@ -405,10 +301,6 @@ let lemma_mod_sub_1 a b =
     b - a%b;
   }
 
-val lemma_mod_mul_distr_l (a:int) (b:int) (n:pos) : Lemma
-  (requires True)
-  (ensures (a * b) % n = ((a % n) * b) % n)
-
 let lemma_mod_mul_distr_l a b n =
   calc (==) {
     (a * b)  % n;
@@ -422,7 +314,6 @@ let lemma_mod_mul_distr_l a b n =
     ((a%n) * b)  % n;
   }
 
-val lemma_mod_mul_distr_r (a:int) (b:int) (n:pos) : Lemma ((a * b) % n = (a * (b % n)) % n)
 let lemma_mod_mul_distr_r (a:int) (b:int) (n:pos) =
   calc (==) {
     (a * b) % n;
@@ -434,29 +325,15 @@ let lemma_mod_mul_distr_r (a:int) (b:int) (n:pos) =
     (a * (b%n)) % n;
   }
 
-val lemma_mod_injective: p:pos -> a:nat -> b:nat -> Lemma
-  (requires (a < p /\ b < p /\ a % p = b % p))
-  (ensures  (a = b))
 let lemma_mod_injective p a b = ()
 
-val lemma_mul_sub_distr: a:int -> b:int -> c:int -> Lemma
-  (a * b - a * c = a * (b - c))
 let lemma_mul_sub_distr a b c =
   distributivity_sub_right a b c
 
-val lemma_div_exact: a:int -> p:pos -> Lemma
-  (requires (a % p = 0))
-  (ensures  (a = p * (a / p)))
 let lemma_div_exact a p = ()
 
-val div_exact_r (a:int) (n:pos) : Lemma
-  (requires (a % n = 0))
-  (ensures  (a = (a / n) * n))
 let div_exact_r (a:int) (n:pos) = lemma_div_exact a n
 
-val lemma_mod_spec: a:int -> p:pos -> Lemma
-  (a / p = (a - (a % p)) / p)
-
 let lemma_mod_spec a p =
   calc (==) {
     (a - a%p)/p;
@@ -466,8 +343,6 @@ let lemma_mod_spec a p =
     a/p;
   }
 
-val lemma_mod_spec2: a:int -> p:pos -> Lemma
-  (let q:int = (a - (a % p)) / p in a = (a % p) + q * p)
 let lemma_mod_spec2 a p =
   calc (==) {
     (a % p) + ((a - (a % p)) / p) * p;
@@ -477,21 +352,14 @@ let lemma_mod_spec2 a p =
     a;
   }
 
-val lemma_mod_plus_distr_l: a:int -> b:int -> p:pos -> Lemma
-  ((a + b) % p = ((a % p) + b) % p)
 let lemma_mod_plus_distr_l a b p =
   let q = (a - (a % p)) / p in
   lemma_mod_spec2 a p;
   lemma_mod_plus (a % p + b) q p
 
-val lemma_mod_plus_distr_r: a:int -> b:int -> p:pos -> Lemma
-  ((a + b) % p = (a + (b % p)) % p)
 let lemma_mod_plus_distr_r a b p =
   lemma_mod_plus_distr_l b a p
 
-val lemma_mod_mod: a:int -> b:int -> p:pos -> Lemma
-  (requires (a = b % p))
-  (ensures  (a % p = b % p))
 let lemma_mod_mod a b p =
   lemma_mod_lt b p;
   modulo_lemma (b % p) p
@@ -502,78 +370,51 @@ let lemma_mod_mod a b p =
 (* * TODO: add triggers for certain lemmas.            **)
 
 (* Lemma: Definition of euclidean division *)
-val euclidean_division_definition: a:int -> b:nonzero ->
-  Lemma (a = (a / b) * b + a % b)
 let euclidean_division_definition a b = ()
 
 (* Lemma: Propriety about modulo *)
-val modulo_range_lemma: a:int -> b:pos ->
-  Lemma (a % b >= 0 && a % b < b)
 let modulo_range_lemma a b = ()
 
-val small_modulo_lemma_1: a:nat -> b:nonzero ->
-  Lemma (requires a < b) (ensures a % b = a)
 let small_modulo_lemma_1 a b = ()
 
-val small_modulo_lemma_2: a:int -> b:pos ->
-  Lemma (requires a % b = a) (ensures a < b)
 let small_modulo_lemma_2 a b = ()
 
-val small_division_lemma_1: a:nat -> b:nonzero ->
-  Lemma (requires a < b) (ensures a / b = 0)
 let small_division_lemma_1 a b = ()
 
-val small_division_lemma_2 (a:int) (n:pos) : Lemma
-  (requires a / n = 0)
-  (ensures 0 <= a /\ a < n)
 let small_division_lemma_2 (a:int) (n:pos) = lemma_div_mod a n
 
 (* Lemma: Multiplication by a positive integer preserves order *)
-val multiplication_order_lemma: a:int -> b:int -> p:pos ->
-  Lemma (a >= b <==> a * p >= b * p)
 let multiplication_order_lemma a b p = ()
 
 (* Lemma: Propriety about multiplication after division *)
-val division_propriety: a:int -> b:pos ->
-  Lemma (a - b < (a / b) * b && (a / b) * b <= a)
 let division_propriety a b = ()
 
 (* Internal lemmas for proving the definition of division *)
-val division_definition_lemma_1: a:int -> b:pos -> m:int{a - b < m * b} ->
-  Lemma (m > a / b - 1)
 let division_definition_lemma_1 a b m =
   if a / b - 1 < 0 then () else begin
     division_propriety a b;
     multiplication_order_lemma m (a / b - 1) b
   end
-val division_definition_lemma_2: a:int -> b:pos -> m:int{m * b <= a} ->
-  Lemma (m < a / b + 1)
+
 let division_definition_lemma_2 a b m =
   division_propriety a b;
   multiplication_order_lemma (a / b + 1) m b
 
 (* Lemma: Definition of division *)
-val division_definition: a:int -> b:pos -> m:int{a - b < m * b && m * b <= a} ->
-  Lemma (m = a / b)
 let division_definition a b m =
   division_definition_lemma_1 a b m;
   division_definition_lemma_2 a b m
 
 (* Lemma: (a * b) / b = a; identical to `cancel_mul_div` above *)
-val multiple_division_lemma (a:int) (n:nonzero) : Lemma ((a * n) / n = a)
 let multiple_division_lemma (a:int) (n:nonzero) = cancel_mul_div a n
 
 (* Lemma: (a * b) % b = 0 *)
-val multiple_modulo_lemma (a:int) (n:pos) : Lemma ((a * n) % n = 0)
 let multiple_modulo_lemma (a:int) (n:pos) = cancel_mul_mod a n
 
 (* Lemma: Division distributivity under special condition *)
-val division_addition_lemma: a:int -> b:pos -> n:int ->
-  Lemma ( (a + n * b) / b = a / b + n )
 let division_addition_lemma a b n = division_definition (a + n * b) b (a / b + n)
 
 (* Lemma: Modulo distributivity *)
-val modulo_distributivity: a:int -> b:int -> c:pos -> Lemma ((a + b) % c == (a % c + b % c) % c)
 let modulo_distributivity a b c =
   calc (==) {
     (a + b) % c;
@@ -583,9 +424,6 @@ let modulo_distributivity a b c =
     ((a % c) + (b % c)) % c;
   }
 
-val lemma_div_le: a:int -> b:int -> d:pos ->
-  Lemma (requires (a <= b))
-        (ensures  (a / d <= b / d))
 let lemma_div_le a b d =
   calc (==>) {
     (a <= b) <: Type0;
@@ -602,13 +440,10 @@ let lemma_div_le a b d =
   }
 
 (* Lemma: Division distributivity under special condition *)
-val division_sub_lemma (a:int) (n:pos) (b:nat) : Lemma ((a - b * n) / n = a / n - b)
 let division_sub_lemma (a:int) (n:pos) (b:nat) =
   neg_mul_left b n;
   lemma_div_plus a (-b) n
 
-val lemma_mod_plus_mul_distr: a:int -> b:int -> c:int -> p:pos -> Lemma
-  (((a + b) * c) % p = ((((a % p) + (b % p)) % p) * (c % p)) % p)
 let lemma_mod_plus_mul_distr a b c p =
   calc (==) {
     ((a + b) * c) % p;
@@ -621,19 +456,13 @@ let lemma_mod_plus_mul_distr a b c p =
   }
 
 (* Lemma: Modulo distributivity under special condition *)
-val modulo_addition_lemma (a:int) (n:pos) (b:int) : Lemma ((a + b * n) % n = a % n)
 let modulo_addition_lemma (a:int) (n:pos) (b:int) = lemma_mod_plus a b n
 
 (* Lemma: Modulo distributivity under special condition *)
-val lemma_mod_sub (a:int) (n:pos) (b:int) : Lemma (ensures (a - b * n) % n = a % n)
 let lemma_mod_sub (a:int) (n:pos) (b:int) =
   neg_mul_left b n;
   lemma_mod_plus a (-b) n
 
-val mod_mult_exact (a:int) (n:pos) (q:pos) : Lemma
-  (requires (a % (n * q) == 0))
-  (ensures a % n == 0)
-
 let mod_mult_exact (a:int) (n:pos) (q:pos) =
   calc (==) {
     a % n;
@@ -648,9 +477,6 @@ let mod_mult_exact (a:int) (n:pos) (q:pos) =
     0;
   }
 
-val mod_mul_div_exact (a:int) (b:pos) (n:pos) : Lemma
-  (requires (a % (b * n) == 0))
-  (ensures (a / b) % n == 0)
 let mod_mul_div_exact (a:int) (b:pos) (n:pos) =
   calc (==) {
     (a / b) % n;
@@ -665,9 +491,6 @@ let mod_mul_div_exact (a:int) (b:pos) (n:pos) =
   }
 
 #push-options "--fuel 1"
-val mod_pow2_div2 (a:int) (m:pos) : Lemma
-  (requires a % pow2 m == 0)
-  (ensures (a / 2) % pow2 (m - 1) == 0)
 let mod_pow2_div2 (a:int) (m:pos) : Lemma
   (requires a % pow2 m == 0)
   (ensures (a / 2) % pow2 (m - 1) == 0)
@@ -705,8 +528,6 @@ private let lemma_mod_mult_zero a b c =
   ()
 
 (* Lemma: Divided by a product is equivalent to being divided one by one *)
-val division_multiplication_lemma (a:int) (b:pos) (c:pos) : Lemma
-  (a / (b * c) = (a / b) / c)
 let division_multiplication_lemma (a:int) (b:pos) (c:pos) =
   calc (==) {
     a / b / c;
@@ -734,7 +555,6 @@ private let cancel_fraction a b c =
     a / b;
   }
 
-val modulo_scale_lemma : a:int -> b:pos -> c:pos -> Lemma ((a * b) % (b * c) == (a % c) * b)
 let modulo_scale_lemma a b c =
   calc (==) {
     (a * b) % (b * c);
@@ -768,9 +588,6 @@ let modulo_division_lemma_0 (a:nat) (b:pos) (c:pos) : Lemma
     division_sub_lemma a b ((a / (b*c)) * c);
     ()
 
-val modulo_division_lemma: a:nat -> b:pos -> c:pos ->
-    Lemma ((a % (b * c)) / b = (a / b) % c)
-
 let modulo_division_lemma a b c =
   calc (==) {
     (a % (b * c)) / b;
@@ -786,9 +603,6 @@ let modulo_division_lemma a b c =
     (a / b) % c;
   }
 
-val modulo_modulo_lemma (a:int) (b:pos) (c:pos) : Lemma
-  ((a % (b * c)) % b = a % b)
-
 let modulo_modulo_lemma (a:int) (b:pos) (c:pos) =
   pos_times_pos_is_pos b c;
   calc (==) {
@@ -811,32 +625,23 @@ let modulo_modulo_lemma (a:int) (b:pos) (c:pos) =
     a % b;
   }
 
-val pow2_multiplication_division_lemma_1: a:int -> b:nat -> c:nat{c >= b} ->
-  Lemma ( (a * pow2 c) / pow2 b = a * pow2 (c - b))
 let pow2_multiplication_division_lemma_1 a b c =
   pow2_plus (c - b) b;
   paren_mul_right a (pow2 (c - b)) (pow2 b);
   paren_mul_left a (pow2 (c - b)) (pow2 b);
   multiple_division_lemma (a * pow2 (c - b)) (pow2 b)
 
-val pow2_multiplication_division_lemma_2: a:int -> b:nat -> c:nat{c <= b} ->
-  Lemma ( (a * pow2 c) / pow2 b = a / pow2 (b - c))
 let pow2_multiplication_division_lemma_2 a b c =
   pow2_plus c (b - c);
   division_multiplication_lemma (a * pow2 c) (pow2 c) (pow2 (b - c));
   multiple_division_lemma a (pow2 c)
 
-val pow2_multiplication_modulo_lemma_1: a:int -> b:nat -> c:nat{c >= b} ->
-  Lemma ( (a * pow2 c) % pow2 b = 0 )
 let pow2_multiplication_modulo_lemma_1 a b c =
   pow2_plus (c - b) b;
   paren_mul_right a (pow2 (c - b)) (pow2 b);
   paren_mul_left a (pow2 (c - b)) (pow2 b);
   multiple_modulo_lemma (a * pow2 (c - b)) (pow2 b)
 
-val pow2_multiplication_modulo_lemma_2: a:int -> b:nat -> c:nat{c <= b} ->
-  Lemma ( (a * pow2 c) % pow2 b = (a % pow2 (b - c)) * pow2 c )
-
 let pow2_multiplication_modulo_lemma_2 a b c =
   calc (==) {
     (a * pow2 c) % pow2 b;
@@ -848,50 +653,31 @@ let pow2_multiplication_modulo_lemma_2 a b c =
     (a % pow2 (b - c)) * pow2 c;
   }
 
-val pow2_modulo_division_lemma_1: a:nat -> b:nat -> c:nat{c >= b} ->
-  Lemma ( (a % pow2 c) / pow2 b = (a / pow2 b) % (pow2 (c - b)) )
 let pow2_modulo_division_lemma_1 a b c =
   pow2_plus (c - b) b;
   modulo_division_lemma a (pow2 b) (pow2 (c - b))
 
-val pow2_modulo_division_lemma_2: a:int -> b:nat -> c:nat{c <= b} ->
-  Lemma ( (a % pow2 c) / pow2 b = 0 )
 let pow2_modulo_division_lemma_2 a b c =
   pow2_le_compat b c;
   small_division_lemma_1 (a % pow2 c) (pow2 b)
 
-val pow2_modulo_modulo_lemma_1: a:int -> b:nat -> c:nat{c >= b} ->
-  Lemma ( (a % pow2 c) % pow2 b = a % pow2 b )
 let pow2_modulo_modulo_lemma_1 a b c =
   pow2_plus (c - b) b;
   modulo_modulo_lemma a (pow2 b) (pow2 (c - b))
 
-val pow2_modulo_modulo_lemma_2: a:int -> b:nat -> c:nat{c <= b} ->
-  Lemma ( (a % pow2 c) % pow2 b = a % pow2 c )
 let pow2_modulo_modulo_lemma_2 a b c =
   pow2_le_compat b c;
   small_modulo_lemma_1 (a % pow2 c) (pow2 b)
 
-val modulo_add : p:pos -> a:int -> b:int -> c:int -> Lemma
-  (requires (b % p = c % p))
-  (ensures  ((a + b) % p = (a + c) % p))
 let modulo_add p a b c =
   modulo_distributivity a b p;
   modulo_distributivity a c p
 
-val lemma_mod_twice : a:int -> p:pos -> Lemma ((a % p) % p == a % p)
 let lemma_mod_twice a p = lemma_mod_mod (a % p) a p
 
-val modulo_sub : p:pos -> a:int -> b:int -> c:int -> Lemma
-  (requires ((a + b) % p = (a + c) % p))
-  (ensures (b % p = c % p))
-
 let modulo_sub p a b c =
   modulo_add p (-a) (a + b) (a + c)
 
-val mod_add_both (a:int) (b:int) (x:int) (n:pos) : Lemma
-  (requires a % n == b % n)
-  (ensures (a + x) % n == (b + x) % n)
 let mod_add_both (a:int) (b:int) (x:int) (n:pos) =
   calc (==) {
     (a + x) % n;
@@ -903,19 +689,12 @@ let mod_add_both (a:int) (b:int) (x:int) (n:pos) =
     (b + x) % n;
   }
 
-val lemma_mod_plus_injective (n:pos) (a:int) (b:nat) (c:nat) : Lemma
-  (requires b < n /\ c < n /\ (a + b) % n = (a + c) % n)
-  (ensures  b = c)
 let lemma_mod_plus_injective (n:pos) (a:int) (b:nat) (c:nat) =
   small_mod b n;
   small_mod c n;
   mod_add_both (a + b) (a + c) (-a) n
 
 (* Another characterization of the modulo *)
-val modulo_sub_lemma (a : int) (b : nat) (c : pos) :
-  Lemma
-  (requires (b < c /\ (a - b) % c = 0))
-  (ensures (b = a % c))
 let modulo_sub_lemma a b c =
   calc (==) {
     b;
diff --git a/ulib/FStar.Math.Lemmas.fsti b/ulib/FStar.Math.Lemmas.fsti
new file mode 100644
index 00000000000..28035ecf357
--- /dev/null
+++ b/ulib/FStar.Math.Lemmas.fsti
@@ -0,0 +1,408 @@
+(*
+   Copyright 2008-2018 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+module FStar.Math.Lemmas
+
+open FStar.Mul
+open FStar.Math.Lib
+
+(* Lemma: definition of Euclidean division *)
+val euclidean_div_axiom: a:int -> b:pos -> Lemma
+  (a - b * (a / b) >= 0 /\ a - b * (a / b) < b)
+
+val lemma_eucl_div_bound: a:int -> b:int -> q:int -> Lemma
+  (requires (a < q))
+  (ensures  (a + q * b < q * (b+1)))
+
+val lemma_mult_le_left: a:nat -> b:int -> c:int -> Lemma
+  (requires (b <= c))
+  (ensures  (a * b <= a * c))
+
+val lemma_mult_le_right: a:nat -> b:int -> c:int -> Lemma
+  (requires (b <= c))
+  (ensures  (b * a <= c * a))
+
+val lemma_mult_lt_left: a:pos -> b:int -> c:int -> Lemma
+  (requires (b < c))
+  (ensures  (a * b < a * c))
+
+val lemma_mult_lt_right: a:pos -> b:int -> c:int -> Lemma
+  (requires (b < c))
+  (ensures  (b * a < c * a))
+
+val lemma_mult_lt_sqr (n:nat) (m:nat) (k:nat{n < k && m < k})
+  : Lemma (n * m < k * k)
+
+(* Lemma: multiplication on integers is commutative *)
+val swap_mul: a:int -> b:int -> Lemma (a * b = b * a)
+
+val lemma_cancel_mul (a b : int) (n : pos) : Lemma (requires (a * n = b * n)) (ensures (a = b))
+
+(* Lemma: multiplication is right distributive over addition *)
+val distributivity_add_left: a:int -> b:int -> c:int -> Lemma
+  ((a + b) * c = a * c + b * c)
+
+(* Lemma: multiplication is left distributive over addition *)
+val distributivity_add_right: a:int -> b:int -> c:int -> Lemma
+  (a * (b + c) = a * b + a * c)
+
+(* Lemma: multiplication is associative, hence parenthesizing is meaningless *)
+(* GM: This is really just an identity since the LHS is associated to the left *)
+val paren_mul_left: a:int -> b:int -> c:int -> Lemma
+  (a * b * c = (a * b) * c)
+
+(* Lemma: multiplication is associative, hence parenthesizing is meaningless *)
+val paren_mul_right: a:int -> b:int -> c:int -> Lemma
+  (a * b * c = a * (b * c))
+
+(* Lemma: addition is associative, hence parenthesizing is meaningless *)
+val paren_add_left: a:int -> b:int -> c:int -> Lemma
+  (a + b + c = (a + b) + c)
+
+(* Lemma: addition is associative, hence parenthesizing is meaningless *)
+val paren_add_right: a:int -> b:int -> c:int -> Lemma
+  (a + b + c = a + (b + c))
+
+val addition_is_associative: a:int -> b:int -> c:int -> Lemma
+  (a + b + c = (a + b) + c /\ a + b + c = a + (b + c))
+
+val subtraction_is_distributive: a:int -> b:int -> c:int -> Lemma
+  (a - b + c = (a - b) + c /\
+   a - b - c = a - (b + c) /\
+   a - b - c = (a - b) - c /\
+   a + (-b - c) = a - b - c /\
+   a - (b - c) = a - b + c)
+
+val swap_add_plus_minus: a:int -> b:int -> c:int -> Lemma
+  (a + b - c = (a - c) + b)
+
+(* Lemma: minus applies to the whole term *)
+val neg_mul_left: a:int -> b:int -> Lemma (-(a * b) = (-a) * b)
+
+(* Lemma: minus applies to the whole term *)
+val neg_mul_right: a:int -> b:int -> Lemma (-(a * b) = a * (-b))
+
+val swap_neg_mul: a:int -> b:int -> Lemma ((-a) * b = a * (-b))
+
+(* Lemma: multiplication is left distributive over subtraction *)
+val distributivity_sub_left: a:int -> b:int -> c:int ->
+  Lemma ((a - b) * c = a * c - b * c)
+
+(* Lemma: multiplication is right distributive over subtraction *)
+val distributivity_sub_right: a:int -> b:int -> c:int ->
+  Lemma ((a * (b - c) = a * b - a * c))
+
+(* Lemma: multiplication precedence on addition *)
+val mul_binds_tighter: a:int -> b:int -> c:int -> Lemma (a + (b * c) = a + b * c)
+
+val lemma_abs_mul : a:int -> b:int -> Lemma (abs a * abs b = abs (a * b))
+
+val lemma_abs_bound : a:int -> b:nat -> Lemma (abs a < b <==> -b < a /\ a < b)
+
+(* Lemma: multiplication keeps symmetric bounds :
+    b > 0 && d > 0 && -b < a < b && -d < c < d ==> - b * d < a * c < b * d *)
+val mul_ineq1: a:int -> b:nat -> c:int -> d:nat -> Lemma
+    (requires (-b < a /\ a < b /\
+               -d < c /\ c < d))
+    (ensures  (-(b * d) < a * c /\ a * c < b * d))
+
+(* Zero is neutral for addition *)
+val add_zero_left_is_same (n : int) : Lemma(0 + n = n)
+val add_zero_right_is_same (n : int) : Lemma(n + 0 = n)
+
+(* One is neutral for multiplication *)
+val mul_one_left_is_same (n : int) : Lemma(1 * n = n)
+val mul_one_right_is_same (n : int) : Lemma(n * 1 = n)
+
+(* Multiplying by zero gives zero *)
+val mul_zero_left_is_zero (n : int) : Lemma(0 * n = 0)
+val mul_zero_right_is_zero (n : int) : Lemma(n * 0 = 0)
+
+val nat_times_nat_is_nat: a:nat -> b:nat -> Lemma (a * b >= 0)
+
+val pos_times_pos_is_pos: a:pos -> b:pos -> Lemma (a * b > 0)
+
+val nat_over_pos_is_nat: a:nat -> b:pos -> Lemma (a / b >= 0)
+
+val nat_plus_nat_equal_zero_lemma: a:nat -> b:nat{a + b = 0} -> Lemma(a = 0 /\ b = 0)
+
+val int_times_int_equal_zero_lemma: a:int -> b:int{a * b = 0} -> Lemma(a = 0 \/ b = 0)
+
+val pow2_double_sum: n:nat -> Lemma (pow2 n + pow2 n = pow2 (n + 1))
+
+val pow2_double_mult: n:nat -> Lemma (2 * pow2 n = pow2 (n + 1))
+
+val pow2_lt_compat: n:nat -> m:nat -> Lemma
+  (requires (m < n))
+  (ensures  (pow2 m < pow2 n))
+  (decreases m)
+
+val pow2_le_compat: n:nat -> m:nat -> Lemma
+  (requires (m <= n))
+  (ensures  (pow2 m <= pow2 n))
+
+val pow2_plus: n:nat -> m:nat -> Lemma
+  (ensures (pow2 n * pow2 m = pow2 (n + m)))
+  (decreases n)
+
+(* Lemma : definition of the exponential property of pow2 *)
+val pow2_minus: n:nat -> m:nat{ n >= m } -> Lemma
+  ((pow2 n) / (pow2 m) = pow2 (n - m))
+
+(* Lemma: loss of precision in euclidean division *)
+val multiply_fractions (a:int) (n:nonzero) : Lemma (n * ( a / n ) <= a)
+
+(** Same as `small_mod` *)
+val modulo_lemma: a:nat -> b:pos -> Lemma (requires (a < b)) (ensures (a % b = a))
+
+(** Same as `lemma_div_def` in Math.Lib *)
+val lemma_div_mod: a:int -> p:nonzero -> Lemma (a = p * (a / p) + a % p)
+
+val lemma_mod_lt: a:int -> p:pos -> Lemma (0 <= a % p /\ a % p < p /\ (a >= 0 ==> a % p <= a))
+
+val lemma_div_lt_nat: a:int -> n:nat -> m:nat{m <= n} ->
+  Lemma (requires (a < pow2 n))
+        (ensures  (a / pow2 m < pow2 (n-m)))
+
+val lemma_div_lt (a:int) (n:nat) (m:nat) : Lemma
+  (requires m <= n /\ a < pow2 n)
+  (ensures a / pow2 m < pow2 (n-m))
+
+val bounded_multiple_is_zero (x:int) (n:pos) : Lemma
+  (requires -n < x * n /\ x * n < n)
+  (ensures x == 0)
+
+val small_div (a:nat) (n:pos) : Lemma (requires a < n) (ensures a / n == 0)
+
+val small_mod (a:nat) (n:pos) : Lemma (requires a < n) (ensures a % n == a)
+
+val lt_multiple_is_equal (a:nat) (b:nat) (x:int) (n:nonzero) : Lemma
+  (requires a < n /\ b < n /\ a == b + x * n)
+  (ensures a == b /\ x == 0)
+
+val lemma_mod_plus (a:int) (k:int) (n:pos) : Lemma ((a + k * n) % n = a % n)
+
+val lemma_div_plus (a:int) (k:int) (n:pos) : Lemma ((a + k * n) / n = a / n + k)
+
+val lemma_div_mod_plus (a:int) (k:int) (n:pos)
+  : Lemma ((a + k * n) / n = a / n + k /\
+           (a + k * n) % n = a % n)
+
+val add_div_mod_1 (a:int) (n:pos)
+  : Lemma ((a + n) % n == a % n /\
+           (a + n) / n == a / n + 1)
+
+val sub_div_mod_1 (a:int) (n:pos)
+  : Lemma ((a - n) % n == a % n /\
+           (a - n) / n == a / n - 1)
+
+val cancel_mul_div (a:int) (n:nonzero) : Lemma ((a * n) / n == a)
+
+val cancel_mul_mod (a:int) (n:pos) : Lemma ((a * n) % n == 0)
+
+val lemma_mod_add_distr (a:int) (b:int) (n:pos) : Lemma ((a + b % n) % n = (a + b) % n)
+
+val lemma_mod_sub_distr (a:int) (b:int) (n:pos) : Lemma ((a - b % n) % n = (a - b) % n)
+
+val lemma_mod_sub_0: a:pos -> Lemma ((-1) % a = a - 1)
+
+val lemma_mod_sub_1: a:pos -> b:pos{a < b} -> Lemma ((-a) % b = b - (a%b))
+
+val lemma_mod_mul_distr_l (a:int) (b:int) (n:pos) : Lemma
+  (requires True)
+  (ensures (a * b) % n = ((a % n) * b) % n)
+
+
+val lemma_mod_mul_distr_r (a:int) (b:int) (n:pos) : Lemma ((a * b) % n = (a * (b % n)) % n)
+
+val lemma_mod_injective: p:pos -> a:nat -> b:nat -> Lemma
+  (requires (a < p /\ b < p /\ a % p = b % p))
+  (ensures  (a = b))
+
+val lemma_mul_sub_distr: a:int -> b:int -> c:int -> Lemma
+  (a * b - a * c = a * (b - c))
+
+val lemma_div_exact: a:int -> p:pos -> Lemma
+  (requires (a % p = 0))
+  (ensures  (a = p * (a / p)))
+
+val div_exact_r (a:int) (n:pos) : Lemma
+  (requires (a % n = 0))
+  (ensures  (a = (a / n) * n))
+
+val lemma_mod_spec: a:int -> p:pos -> Lemma
+  (a / p = (a - (a % p)) / p)
+
+val lemma_mod_spec2: a:int -> p:pos -> Lemma
+  (let q:int = (a - (a % p)) / p in a = (a % p) + q * p)
+
+val lemma_mod_plus_distr_l: a:int -> b:int -> p:pos -> Lemma
+  ((a + b) % p = ((a % p) + b) % p)
+
+val lemma_mod_plus_distr_r: a:int -> b:int -> p:pos -> Lemma
+  ((a + b) % p = (a + (b % p)) % p)
+
+val lemma_mod_mod: a:int -> b:int -> p:pos -> Lemma
+  (requires (a = b % p))
+  (ensures  (a % p = b % p))
+
+(* * Lemmas about multiplication, division and modulo. **)
+(* * This part focuses on the situation where          **)
+(* * dividend: nat    divisor: pos                     **)
+(* * TODO: add triggers for certain lemmas.            **)
+
+(* Lemma: Definition of euclidean division *)
+val euclidean_division_definition: a:int -> b:nonzero ->
+  Lemma (a = (a / b) * b + a % b)
+
+(* Lemma: Propriety about modulo *)
+val modulo_range_lemma: a:int -> b:pos ->
+  Lemma (a % b >= 0 && a % b < b)
+
+val small_modulo_lemma_1: a:nat -> b:nonzero ->
+  Lemma (requires a < b) (ensures a % b = a)
+
+val small_modulo_lemma_2: a:int -> b:pos ->
+  Lemma (requires a % b = a) (ensures a < b)
+
+val small_division_lemma_1: a:nat -> b:nonzero ->
+  Lemma (requires a < b) (ensures a / b = 0)
+
+val small_division_lemma_2 (a:int) (n:pos) : Lemma
+  (requires a / n = 0)
+  (ensures 0 <= a /\ a < n)
+
+(* Lemma: Multiplication by a positive integer preserves order *)
+val multiplication_order_lemma: a:int -> b:int -> p:pos ->
+  Lemma (a >= b <==> a * p >= b * p)
+
+(* Lemma: Propriety about multiplication after division *)
+val division_propriety: a:int -> b:pos ->
+  Lemma (a - b < (a / b) * b && (a / b) * b <= a)
+
+(* Internal lemmas for proving the definition of division *)
+val division_definition_lemma_1: a:int -> b:pos -> m:int{a - b < m * b} ->
+  Lemma (m > a / b - 1)
+
+val division_definition_lemma_2: a:int -> b:pos -> m:int{m * b <= a} ->
+  Lemma (m < a / b + 1)
+
+(* Lemma: Definition of division *)
+val division_definition: a:int -> b:pos -> m:int{a - b < m * b && m * b <= a} ->
+  Lemma (m = a / b)
+
+(* Lemma: (a * b) / b = a; identical to `cancel_mul_div` above *)
+val multiple_division_lemma (a:int) (n:nonzero) : Lemma ((a * n) / n = a)
+
+(* Lemma: (a * b) % b = 0 *)
+val multiple_modulo_lemma (a:int) (n:pos) : Lemma ((a * n) % n = 0)
+
+(* Lemma: Division distributivity under special condition *)
+val division_addition_lemma: a:int -> b:pos -> n:int ->
+  Lemma ( (a + n * b) / b = a / b + n )
+
+(* Lemma: Modulo distributivity *)
+val modulo_distributivity: a:int -> b:int -> c:pos -> Lemma ((a + b) % c == (a % c + b % c) % c)
+
+val lemma_div_le: a:int -> b:int -> d:pos ->
+  Lemma (requires (a <= b))
+        (ensures  (a / d <= b / d))
+
+(* Lemma: Division distributivity under special condition *)
+val division_sub_lemma (a:int) (n:pos) (b:nat) : Lemma ((a - b * n) / n = a / n - b)
+
+val lemma_mod_plus_mul_distr: a:int -> b:int -> c:int -> p:pos -> Lemma
+  (((a + b) * c) % p = ((((a % p) + (b % p)) % p) * (c % p)) % p)
+
+(* Lemma: Modulo distributivity under special condition *)
+val modulo_addition_lemma (a:int) (n:pos) (b:int) : Lemma ((a + b * n) % n = a % n)
+
+(* Lemma: Modulo distributivity under special condition *)
+val lemma_mod_sub (a:int) (n:pos) (b:int) : Lemma (ensures (a - b * n) % n = a % n)
+
+val mod_mult_exact (a:int) (n:pos) (q:pos) : Lemma
+  (requires (a % (n * q) == 0))
+  (ensures a % n == 0)
+
+val mod_mul_div_exact (a:int) (b:pos) (n:pos) : Lemma
+  (requires (a % (b * n) == 0))
+  (ensures (a / b) % n == 0)
+
+val mod_pow2_div2 (a:int) (m:pos) : Lemma
+  (requires a % pow2 m == 0)
+  (ensures (a / 2) % pow2 (m - 1) == 0)
+
+(* Lemma: Divided by a product is equivalent to being divided one by one *)
+val division_multiplication_lemma (a:int) (b:pos) (c:pos) : Lemma
+  (a / (b * c) = (a / b) / c)
+
+val modulo_scale_lemma : a:int -> b:pos -> c:pos -> Lemma ((a * b) % (b * c) == (a % c) * b)
+
+val lemma_mul_pos_pos_is_pos (x:pos) (y:pos) : Lemma (x*y > 0)
+val lemma_mul_nat_pos_is_nat (x:nat) (y:pos) : Lemma (x*y >= 0)
+
+val modulo_division_lemma: a:nat -> b:pos -> c:pos ->
+    Lemma ((a % (b * c)) / b = (a / b) % c)
+
+val modulo_modulo_lemma (a:int) (b:pos) (c:pos) : Lemma
+  ((a % (b * c)) % b = a % b)
+
+val pow2_multiplication_division_lemma_1: a:int -> b:nat -> c:nat{c >= b} ->
+  Lemma ( (a * pow2 c) / pow2 b = a * pow2 (c - b))
+
+val pow2_multiplication_division_lemma_2: a:int -> b:nat -> c:nat{c <= b} ->
+  Lemma ( (a * pow2 c) / pow2 b = a / pow2 (b - c))
+
+val pow2_multiplication_modulo_lemma_1: a:int -> b:nat -> c:nat{c >= b} ->
+  Lemma ( (a * pow2 c) % pow2 b = 0 )
+
+val pow2_multiplication_modulo_lemma_2: a:int -> b:nat -> c:nat{c <= b} ->
+  Lemma ( (a * pow2 c) % pow2 b = (a % pow2 (b - c)) * pow2 c )
+
+val pow2_modulo_division_lemma_1: a:nat -> b:nat -> c:nat{c >= b} ->
+  Lemma ( (a % pow2 c) / pow2 b = (a / pow2 b) % (pow2 (c - b)) )
+
+val pow2_modulo_division_lemma_2: a:int -> b:nat -> c:nat{c <= b} ->
+  Lemma ( (a % pow2 c) / pow2 b = 0 )
+
+val pow2_modulo_modulo_lemma_1: a:int -> b:nat -> c:nat{c >= b} ->
+  Lemma ( (a % pow2 c) % pow2 b = a % pow2 b )
+
+val pow2_modulo_modulo_lemma_2: a:int -> b:nat -> c:nat{c <= b} ->
+  Lemma ( (a % pow2 c) % pow2 b = a % pow2 c )
+
+val modulo_add : p:pos -> a:int -> b:int -> c:int -> Lemma
+  (requires (b % p = c % p))
+  (ensures  ((a + b) % p = (a + c) % p))
+
+val lemma_mod_twice : a:int -> p:pos -> Lemma ((a % p) % p == a % p)
+
+val modulo_sub : p:pos -> a:int -> b:int -> c:int -> Lemma
+  (requires ((a + b) % p = (a + c) % p))
+  (ensures (b % p = c % p))
+
+val mod_add_both (a:int) (b:int) (x:int) (n:pos) : Lemma
+  (requires a % n == b % n)
+  (ensures (a + x) % n == (b + x) % n)
+
+val lemma_mod_plus_injective (n:pos) (a:int) (b:nat) (c:nat) : Lemma
+  (requires b < n /\ c < n /\ (a + b) % n = (a + c) % n)
+  (ensures  b = c)
+
+(* Another characterization of the modulo *)
+val modulo_sub_lemma (a : int) (b : nat) (c : pos) :
+  Lemma
+  (requires (b < c /\ (a - b) % c = 0))
+  (ensures (b = a % c))
\ No newline at end of file