diff --git a/library/init/data/int/comp_lemmas.lean b/library/init/data/int/comp_lemmas.lean
index 8bebf61677..c9a339cc45 100644
--- a/library/init/data/int/comp_lemmas.lean
+++ b/library/init/data/int/comp_lemmas.lean
@@ -13,9 +13,18 @@ namespace int
 
 /- 1. Lemmas for reducing the problem to the case where the numerals are positive -/
 
-protected lemma ne_neg_of_ne (a b : ℤ) : a ≠ b → -a ≠ -b :=
+protected lemma ne_neg_of_ne {a b : ℤ} : a ≠ b → -a ≠ -b :=
 λ h₁ h₂, absurd (neg_inj h₂) h₁
 
+protected lemma neg_ne_zero_of_ne {a : ℤ} : a ≠ 0 → -a ≠ 0 :=
+λ h₁ h₂,
+  have -a = -0, by rwa neg_zero,
+  have a = 0, from neg_inj this,
+  by contradiction
+
+protected lemma zero_ne_neg_of_ne {a : ℤ} (h : 0 ≠ a) : 0 ≠ -a :=
+ne.symm (int.neg_ne_zero_of_ne (ne.symm h))
+
 protected lemma neg_ne_of_pos {a b : ℤ} : a > 0 → b > 0 → -a ≠ b :=
 λ h₁ h₂ h,
 begin
@@ -69,9 +78,9 @@ assume h,
   have of_nat (nat_abs a) = of_nat (nat_abs b), by rwa [of_nat_nat_abs_eq_of_nonneg ha, of_nat_nat_abs_eq_of_nonneg hb],
   begin injection this, contradiction end
 
-protected lemma ne_of_nat_ne_pos_case {a b : ℤ} {n m : nat} (ha : a > 0) (hb : b > 0) (e1 : nat_abs a = n) (e2 : nat_abs b = m) (h : n ≠ m) : a ≠ b :=
+protected lemma ne_of_nat_ne_nonneg_case {a b : ℤ} {n m : nat} (ha : a ≥ 0) (hb : b ≥ 0) (e1 : nat_abs a = n) (e2 : nat_abs b = m) (h : n ≠ m) : a ≠ b :=
 have nat_abs a ≠ nat_abs b, by rwa [e1, e2],
-ne_of_nat_abs_ne_nat_abs_of_nonneg (le_of_lt ha) (le_of_lt hb) this
+ne_of_nat_abs_ne_nat_abs_of_nonneg ha hb this
 
 /- 4. Aux lemmas for pushing nat_abs inside numerals
    nat_abs_zero and nat_abs_one are defined at init/data/int/basic.lean -/
diff --git a/library/init/meta/comp_value_tactics.lean b/library/init/meta/comp_value_tactics.lean
index 65019e3276..1cb517a098 100644
--- a/library/init/meta/comp_value_tactics.lean
+++ b/library/init/meta/comp_value_tactics.lean
@@ -12,6 +12,7 @@ meta constant mk_nat_val_le_proof : expr → expr → option expr
 meta constant mk_fin_val_ne_proof : expr → expr → option expr
 meta constant mk_char_val_ne_proof : expr → expr → option expr
 meta constant mk_string_val_ne_proof : expr → expr → option expr
+meta constant mk_int_val_ne_proof : expr → expr → option expr
 
 namespace tactic
 open expr
@@ -50,6 +51,11 @@ do t ← target,
        pr     ← returnopt (mk_string_val_ne_proof a b),
        exact pr)
    <|>
+   (do is_def_eq type (const `int []),
+       (a, b) ← returnopt (is_ne t),
+       pr     ← returnopt (mk_int_val_ne_proof a b),
+       exact pr)
+   <|>
    (do type   ← whnf type,
        guard (is_napp_of type `fin 1),
        (a, b) ← returnopt (is_ne t),
diff --git a/src/library/comp_val.cpp b/src/library/comp_val.cpp
index 123623cae9..9c67c620bc 100644
--- a/src/library/comp_val.cpp
+++ b/src/library/comp_val.cpp
@@ -8,6 +8,12 @@ Author: Leonardo de Moura
 #include "library/string.h"
 #include "library/util.h"
 #include "library/constants.h"
+#include "library/comp_val.h"
+#include "library/expr_pair.h"
+#include "library/trace.h"
+
+/* Remark: we can improve performance by using Lean macros for delaying the
+   proof construction. */
 
 namespace lean {
 optional<expr> mk_nat_val_ne_proof(expr const & a, expr const & b) {
@@ -178,6 +184,110 @@ optional<expr> mk_string_val_ne_proof(expr a, expr b) {
     return none_expr();
 }
 
+optional<expr> mk_int_val_nonneg_proof(expr const & a) {
+    if (auto a1 = is_bit0(a)) {
+        if (auto pr = mk_int_val_nonneg_proof(*a1))
+            return some_expr(mk_app(mk_constant(get_int_bit0_nonneg_name()), *a1, *pr));
+    } else if (auto a1 = is_bit1(a)) {
+        if (auto pr = mk_int_val_nonneg_proof(*a1))
+            return some_expr(mk_app(mk_constant(get_int_bit1_nonneg_name()), *a1, *pr));
+    } else if (is_one(a)) {
+        return some_expr(mk_constant(get_int_one_nonneg_name()));
+    } else if (is_zero(a)) {
+        return some_expr(mk_constant(get_int_zero_nonneg_name()));
+    }
+    return none_expr();
+}
+
+optional<expr> mk_int_val_pos_proof(expr const & a) {
+    if (auto a1 = is_bit0(a)) {
+        if (auto pr = mk_int_val_pos_proof(*a1))
+            return some_expr(mk_app(mk_constant(get_int_bit0_pos_name()), *a1, *pr));
+    } else if (auto a1 = is_bit1(a)) {
+        if (auto pr = mk_int_val_nonneg_proof(*a1))
+            return some_expr(mk_app(mk_constant(get_int_bit1_pos_name()), *a1, *pr));
+    } else if (is_one(a)) {
+        return some_expr(mk_constant(get_int_one_pos_name()));
+    }
+    return none_expr();
+}
+
+/* Given a nonnegative int numeral a, return a pair (n, H)
+   where n is a nat numeral, and (H : nat_abs a = n) */
+optional<expr_pair> mk_nat_abs_eq(expr const & a) {
+    if (is_zero(a)) {
+        return optional<expr_pair>(mk_pair(mk_nat_zero(), mk_constant(get_int_nat_abs_zero_name())));
+    } else if (is_one(a)) {
+        return optional<expr_pair>(mk_pair(mk_nat_one(), mk_constant(get_int_nat_abs_one_name())));
+    } else if (auto a1 = is_bit0(a)) {
+        if (auto p = mk_nat_abs_eq(*a1))
+            return optional<expr_pair>(mk_pair(mk_nat_bit0(p->first),
+                                               mk_app(mk_constant(get_int_nat_abs_bit0_step_name()), *a1, p->first, p->second)));
+    } else if (auto a1 = is_bit1(a)) {
+        if (auto p = mk_nat_abs_eq(*a1)) {
+            expr new_n   = mk_nat_bit1(p->first);
+            expr Hnonneg = *mk_int_val_nonneg_proof(*a1);
+            expr new_H   = mk_app(mk_constant(get_int_nat_abs_bit1_nonneg_step_name()), *a1, p->first, Hnonneg, p->second);
+            return optional<expr_pair>(mk_pair(new_n, new_H));
+        }
+    }
+    return optional<expr_pair>();
+}
+
+/* Given nonneg int numerals a and b, create a proof for a != b IF they are not equal. */
+optional<expr> mk_int_nonneg_val_ne_proof(expr const & a, expr const & b) {
+    auto p1 = mk_nat_abs_eq(a);
+    if (!p1) return none_expr();
+    auto p2 = mk_nat_abs_eq(b);
+    if (!p2) return none_expr();
+    auto Ha_nonneg = mk_int_val_nonneg_proof(a);
+    if (!Ha_nonneg) return none_expr();
+    auto Hb_nonneg = mk_int_val_nonneg_proof(a);
+    if (!Hb_nonneg) return none_expr();
+    auto H_nat_ne  = mk_nat_val_ne_proof(p1->first, p2->first);
+    if (!H_nat_ne) return none_expr();
+    expr H = mk_app({mk_constant(get_int_ne_of_nat_ne_nonneg_case_name()), a, b, p1->first, p2->first,
+                *Ha_nonneg, *Hb_nonneg, p1->second, p2->second, *H_nat_ne});
+    return some_expr(H);
+}
+
+optional<expr> mk_int_val_ne_proof(expr const & a, expr const & b) {
+    if (auto a1 = is_neg(a)) {
+        if (auto b1 = is_neg(b)) {
+            auto H = mk_int_nonneg_val_ne_proof(*a1, *b1);
+            if (!H) return none_expr();
+            return some_expr(mk_app(mk_constant(get_int_ne_neg_of_ne_name()), *a1, *b1, *H));
+        } else {
+            if (is_zero(b)) {
+                auto H = mk_int_nonneg_val_ne_proof(*a1, b);
+                if (!H) return none_expr();
+                return some_expr(mk_app(mk_constant(get_int_neg_ne_zero_of_ne_name()), *a1, *H));
+            } else {
+                auto Ha1_nonneg = mk_int_val_pos_proof(*a1);
+                if (!Ha1_nonneg) return none_expr();
+                auto Hb_nonneg  = mk_int_val_pos_proof(b);
+                if (!Hb_nonneg) return none_expr();
+                return some_expr(mk_app(mk_constant(get_int_neg_ne_of_pos_name()), *a1, b, *Ha1_nonneg, *Hb_nonneg));
+            }
+        }
+    } else {
+        if (auto b1 = is_neg(b)) {
+            if (is_zero(a)) {
+                auto H = mk_int_nonneg_val_ne_proof(a, *b1);
+                if (!H) return none_expr();
+                return some_expr(mk_app(mk_constant(get_int_zero_ne_neg_of_ne_name()), *b1, *H));
+            } else {
+                auto Ha_nonneg = mk_int_val_pos_proof(a);
+                if (!Ha_nonneg) return none_expr();
+                auto Hb1_nonneg = mk_int_val_pos_proof(*b1);
+                return some_expr(mk_app(mk_constant(get_int_ne_neg_of_pos_name()), a, *b1, *Ha_nonneg, *Hb1_nonneg));
+            }
+        } else {
+            return mk_int_nonneg_val_ne_proof(a, b);
+        }
+    }
+}
+
 void initialize_comp_val() {
     g_char_sz = new expr(to_nat_expr(mpz(256)));
 }
diff --git a/src/library/comp_val.h b/src/library/comp_val.h
index 5f79fc3e71..b8992223ee 100644
--- a/src/library/comp_val.h
+++ b/src/library/comp_val.h
@@ -31,12 +31,25 @@ optional<expr> mk_nat_val_le_proof(expr const & a, expr const & b);
 /* Similar to mk_nat_val_ne_proof, but for fin type */
 optional<expr> mk_fin_val_ne_proof(expr const & a, expr const & b);
 
-/* Similar to mk_char_val_ne_proof, but for char type */
+/* Similar to mk_nat_val_ne_proof, but for char type */
 optional<expr> mk_char_val_ne_proof(expr const & a, expr const & b);
 
-/* Similar to mk_char_val_ne_proof, but for string type */
+/* Similar to mk_nat_val_ne_proof, but for string type */
 optional<expr> mk_string_val_ne_proof(expr a, expr b);
 
+/* Return a proof for e >= 0 if e is a nonnegative int numeral.
+
+   \pre typeof(e) is int. */
+optional<expr> mk_int_val_nonneg_proof(expr const & e);
+
+/* Return a proof for e > 0 if e is a nonnegative int numeral.
+
+   \pre typeof(e) is int. */
+optional<expr> mk_int_val_pos_proof(expr const & a);
+
+/* Similar to mk_nat_val_ne_proof, but for int type */
+optional<expr> mk_int_val_ne_proof(expr const & a, expr const & b);
+
 void initialize_comp_val();
 void finalize_comp_val();
 }
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index b82e393817..c20ee44eac 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -147,6 +147,23 @@ name const * g_int_has_le = nullptr;
 name const * g_int_has_lt = nullptr;
 name const * g_int_has_neg = nullptr;
 name const * g_int_has_mod = nullptr;
+name const * g_int_bit0_nonneg = nullptr;
+name const * g_int_bit1_nonneg = nullptr;
+name const * g_int_one_nonneg = nullptr;
+name const * g_int_zero_nonneg = nullptr;
+name const * g_int_bit0_pos = nullptr;
+name const * g_int_bit1_pos = nullptr;
+name const * g_int_one_pos = nullptr;
+name const * g_int_nat_abs_zero = nullptr;
+name const * g_int_nat_abs_one = nullptr;
+name const * g_int_nat_abs_bit0_step = nullptr;
+name const * g_int_nat_abs_bit1_nonneg_step = nullptr;
+name const * g_int_ne_of_nat_ne_nonneg_case = nullptr;
+name const * g_int_ne_neg_of_ne = nullptr;
+name const * g_int_neg_ne_of_pos = nullptr;
+name const * g_int_ne_neg_of_pos = nullptr;
+name const * g_int_neg_ne_zero_of_ne = nullptr;
+name const * g_int_zero_ne_neg_of_ne = nullptr;
 name const * g_int_decidable_linear_ordered_comm_group = nullptr;
 name const * g_io = nullptr;
 name const * g_io_functor = nullptr;
@@ -579,6 +596,23 @@ void initialize_constants() {
     g_int_has_lt = new name{"int", "has_lt"};
     g_int_has_neg = new name{"int", "has_neg"};
     g_int_has_mod = new name{"int", "has_mod"};
+    g_int_bit0_nonneg = new name{"int", "bit0_nonneg"};
+    g_int_bit1_nonneg = new name{"int", "bit1_nonneg"};
+    g_int_one_nonneg = new name{"int", "one_nonneg"};
+    g_int_zero_nonneg = new name{"int", "zero_nonneg"};
+    g_int_bit0_pos = new name{"int", "bit0_pos"};
+    g_int_bit1_pos = new name{"int", "bit1_pos"};
+    g_int_one_pos = new name{"int", "one_pos"};
+    g_int_nat_abs_zero = new name{"int", "nat_abs_zero"};
+    g_int_nat_abs_one = new name{"int", "nat_abs_one"};
+    g_int_nat_abs_bit0_step = new name{"int", "nat_abs_bit0_step"};
+    g_int_nat_abs_bit1_nonneg_step = new name{"int", "nat_abs_bit1_nonneg_step"};
+    g_int_ne_of_nat_ne_nonneg_case = new name{"int", "ne_of_nat_ne_nonneg_case"};
+    g_int_ne_neg_of_ne = new name{"int", "ne_neg_of_ne"};
+    g_int_neg_ne_of_pos = new name{"int", "neg_ne_of_pos"};
+    g_int_ne_neg_of_pos = new name{"int", "ne_neg_of_pos"};
+    g_int_neg_ne_zero_of_ne = new name{"int", "neg_ne_zero_of_ne"};
+    g_int_zero_ne_neg_of_ne = new name{"int", "zero_ne_neg_of_ne"};
     g_int_decidable_linear_ordered_comm_group = new name{"int_decidable_linear_ordered_comm_group"};
     g_io = new name{"io"};
     g_io_functor = new name{"io", "functor"};
@@ -1012,6 +1046,23 @@ void finalize_constants() {
     delete g_int_has_lt;
     delete g_int_has_neg;
     delete g_int_has_mod;
+    delete g_int_bit0_nonneg;
+    delete g_int_bit1_nonneg;
+    delete g_int_one_nonneg;
+    delete g_int_zero_nonneg;
+    delete g_int_bit0_pos;
+    delete g_int_bit1_pos;
+    delete g_int_one_pos;
+    delete g_int_nat_abs_zero;
+    delete g_int_nat_abs_one;
+    delete g_int_nat_abs_bit0_step;
+    delete g_int_nat_abs_bit1_nonneg_step;
+    delete g_int_ne_of_nat_ne_nonneg_case;
+    delete g_int_ne_neg_of_ne;
+    delete g_int_neg_ne_of_pos;
+    delete g_int_ne_neg_of_pos;
+    delete g_int_neg_ne_zero_of_ne;
+    delete g_int_zero_ne_neg_of_ne;
     delete g_int_decidable_linear_ordered_comm_group;
     delete g_io;
     delete g_io_functor;
@@ -1444,6 +1495,23 @@ name const & get_int_has_le_name() { return *g_int_has_le; }
 name const & get_int_has_lt_name() { return *g_int_has_lt; }
 name const & get_int_has_neg_name() { return *g_int_has_neg; }
 name const & get_int_has_mod_name() { return *g_int_has_mod; }
+name const & get_int_bit0_nonneg_name() { return *g_int_bit0_nonneg; }
+name const & get_int_bit1_nonneg_name() { return *g_int_bit1_nonneg; }
+name const & get_int_one_nonneg_name() { return *g_int_one_nonneg; }
+name const & get_int_zero_nonneg_name() { return *g_int_zero_nonneg; }
+name const & get_int_bit0_pos_name() { return *g_int_bit0_pos; }
+name const & get_int_bit1_pos_name() { return *g_int_bit1_pos; }
+name const & get_int_one_pos_name() { return *g_int_one_pos; }
+name const & get_int_nat_abs_zero_name() { return *g_int_nat_abs_zero; }
+name const & get_int_nat_abs_one_name() { return *g_int_nat_abs_one; }
+name const & get_int_nat_abs_bit0_step_name() { return *g_int_nat_abs_bit0_step; }
+name const & get_int_nat_abs_bit1_nonneg_step_name() { return *g_int_nat_abs_bit1_nonneg_step; }
+name const & get_int_ne_of_nat_ne_nonneg_case_name() { return *g_int_ne_of_nat_ne_nonneg_case; }
+name const & get_int_ne_neg_of_ne_name() { return *g_int_ne_neg_of_ne; }
+name const & get_int_neg_ne_of_pos_name() { return *g_int_neg_ne_of_pos; }
+name const & get_int_ne_neg_of_pos_name() { return *g_int_ne_neg_of_pos; }
+name const & get_int_neg_ne_zero_of_ne_name() { return *g_int_neg_ne_zero_of_ne; }
+name const & get_int_zero_ne_neg_of_ne_name() { return *g_int_zero_ne_neg_of_ne; }
 name const & get_int_decidable_linear_ordered_comm_group_name() { return *g_int_decidable_linear_ordered_comm_group; }
 name const & get_io_name() { return *g_io; }
 name const & get_io_functor_name() { return *g_io_functor; }
diff --git a/src/library/constants.h b/src/library/constants.h
index 4b769b5dd5..88af109092 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -149,6 +149,23 @@ name const & get_int_has_le_name();
 name const & get_int_has_lt_name();
 name const & get_int_has_neg_name();
 name const & get_int_has_mod_name();
+name const & get_int_bit0_nonneg_name();
+name const & get_int_bit1_nonneg_name();
+name const & get_int_one_nonneg_name();
+name const & get_int_zero_nonneg_name();
+name const & get_int_bit0_pos_name();
+name const & get_int_bit1_pos_name();
+name const & get_int_one_pos_name();
+name const & get_int_nat_abs_zero_name();
+name const & get_int_nat_abs_one_name();
+name const & get_int_nat_abs_bit0_step_name();
+name const & get_int_nat_abs_bit1_nonneg_step_name();
+name const & get_int_ne_of_nat_ne_nonneg_case_name();
+name const & get_int_ne_neg_of_ne_name();
+name const & get_int_neg_ne_of_pos_name();
+name const & get_int_ne_neg_of_pos_name();
+name const & get_int_neg_ne_zero_of_ne_name();
+name const & get_int_zero_ne_neg_of_ne_name();
 name const & get_int_decidable_linear_ordered_comm_group_name();
 name const & get_io_name();
 name const & get_io_functor_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index bc06b235f8..5a189e61f0 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -142,6 +142,23 @@ int.has_le
 int.has_lt
 int.has_neg
 int.has_mod
+int.bit0_nonneg
+int.bit1_nonneg
+int.one_nonneg
+int.zero_nonneg
+int.bit0_pos
+int.bit1_pos
+int.one_pos
+int.nat_abs_zero
+int.nat_abs_one
+int.nat_abs_bit0_step
+int.nat_abs_bit1_nonneg_step
+int.ne_of_nat_ne_nonneg_case
+int.ne_neg_of_ne
+int.neg_ne_of_pos
+int.ne_neg_of_pos
+int.neg_ne_zero_of_ne
+int.zero_ne_neg_of_ne
 int_decidable_linear_ordered_comm_group
 io
 io.functor
diff --git a/src/library/norm_num.h b/src/library/norm_num.h
index 980c770d1d..79b1e9f9ea 100644
--- a/src/library/norm_num.h
+++ b/src/library/norm_num.h
@@ -80,8 +80,6 @@ public:
     expr from_mpq(mpq const &, expr const &);
 };
 
-inline bool is_neg(expr const & e);
-
 inline bool is_numeral(type_context & type_ctx, expr const & e) {
     return norm_num_context(type_ctx).is_numeral(e);
 }
diff --git a/src/library/num.cpp b/src/library/num.cpp
index 2757679341..1ba9542408 100644
--- a/src/library/num.cpp
+++ b/src/library/num.cpp
@@ -73,6 +73,15 @@ bool is_num(expr const & e) {
     return is_num(e, true);
 }
 
+bool is_signed_num(expr const & e) {
+    if (is_num(e))
+        return true;
+    else if (auto r = is_neg(e))
+        return is_num(*r);
+    else
+        return false;
+}
+
 static optional<mpz> to_num(expr const & e, bool first) {
     if (is_zero(e)) {
         return first ? some(mpz(0)) : optional<mpz>();
diff --git a/src/library/num.h b/src/library/num.h
index 918ace2947..fe037139c5 100644
--- a/src/library/num.h
+++ b/src/library/num.h
@@ -13,10 +13,14 @@ bool is_const_app(expr const &, name const &, unsigned);
 /** \brief Return true iff the given expression encodes a numeral. */
 bool is_num(expr const & e);
 
+/** \brief Return true iff is_num(e) or \c e is of the form (- e') where to_num(e') */
+bool is_signed_num(expr const & e);
+
 bool is_zero(expr const & e);
 bool is_one(expr const & e);
 optional<expr> is_bit0(expr const & e);
 optional<expr> is_bit1(expr const & e);
+optional<expr> is_neg(expr const & e);
 
 /** \brief Return true iff \c n is zero, one, bit0 or bit1 */
 bool is_numeral_const_name(name const & n);
diff --git a/src/library/util.cpp b/src/library/util.cpp
index d4adda00d9..db52dec5d2 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -461,24 +461,37 @@ expr mk_snd(abstract_type_context & ctx, expr const & p) {
     return mk_app(mk_constant(get_prod_snd_name(), const_levels(get_app_fn(AxB))), A, B, p);
 }
 
-static expr * g_nat = nullptr;
+static expr * g_nat         = nullptr;
+static expr * g_nat_zero    = nullptr;
+static expr * g_nat_one     = nullptr;
+static expr * g_nat_bit0_fn = nullptr;
+static expr * g_nat_bit1_fn = nullptr;
+static expr * g_nat_add_fn  = nullptr;
 
-expr mk_nat() {
-    return *g_nat;
+static void initialize_nat() {
+    g_nat            = new expr(mk_constant(get_nat_name()));
+    g_nat_zero       = new expr(mk_app(mk_constant(get_zero_name(), {mk_level_one()}), {*g_nat, mk_constant(get_nat_has_zero_name())}));
+    g_nat_one        = new expr(mk_app(mk_constant(get_one_name(), {mk_level_one()}), {*g_nat, mk_constant(get_nat_has_one_name())}));
+    g_nat_bit0_fn    = new expr(mk_app(mk_constant(get_bit0_name(), {mk_level_one()}), {*g_nat, mk_constant(get_nat_has_add_name())}));
+    g_nat_bit1_fn    = new expr(mk_app(mk_constant(get_bit1_name(), {mk_level_one()}), {*g_nat, mk_constant(get_nat_has_one_name()), mk_constant(get_nat_has_add_name())}));
+    g_nat_add_fn     = new expr(mk_app(mk_constant(get_add_name(), {mk_level_one()}), {*g_nat, mk_constant(get_nat_has_add_name())}));
 }
 
-expr mk_nat_zero() {
-    return mk_app(mk_constant(get_zero_name(), {mk_level_one()}), {*g_nat, mk_constant(get_nat_has_zero_name())});
+static void finalize_nat() {
+    delete g_nat;
+    delete g_nat_zero;
+    delete g_nat_one;
+    delete g_nat_bit0_fn;
+    delete g_nat_bit1_fn;
+    delete g_nat_add_fn;
 }
 
-expr mk_nat_one() {
-    return mk_app(mk_constant(get_one_name(), {mk_level_one()}), {*g_nat, mk_constant(get_nat_has_one_name())});
-}
-
-expr mk_nat_add(expr const & e1, expr const & e2) {
-    expr nat_add = mk_app(mk_constant(get_add_name(), {mk_level_one()}), {*g_nat, mk_constant(get_nat_has_add_name())});
-    return mk_app(nat_add, e1, e2);
-}
+expr mk_nat() { return *g_nat; }
+expr mk_nat_zero() { return *g_nat_zero; }
+expr mk_nat_one() { return *g_nat_one; }
+expr mk_nat_bit0(expr const & e) { return mk_app(*g_nat_bit0_fn, e); }
+expr mk_nat_bit1(expr const & e) { return mk_app(*g_nat_bit1_fn, e); }
+expr mk_nat_add(expr const & e1, expr const & e2) { return mk_app(*g_nat_add_fn, e1, e2); }
 
 expr mk_unit(level const & l, bool prop) { return prop ? mk_true() : mk_unit(l); }
 expr mk_unit_mk(level const & l, bool prop) { return prop ? mk_true_intro() : mk_unit_mk(l); }
@@ -948,11 +961,11 @@ void initialize_library_util() {
     g_and_intro      = new expr(mk_constant(get_and_intro_name()));
     g_and_elim_left  = new expr(mk_constant(get_and_elim_left_name()));
     g_and_elim_right = new expr(mk_constant(get_and_elim_right_name()));
-    g_nat            = new expr(mk_constant(get_nat_name()));
+    initialize_nat();
 }
 
 void finalize_library_util() {
-    delete g_nat;
+    finalize_nat();
     delete g_true;
     delete g_true_intro;
     delete g_and;
diff --git a/src/library/util.h b/src/library/util.h
index a77a6d3c49..149bea9bfc 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -176,6 +176,8 @@ expr mk_snd(abstract_type_context & ctx, expr const & p, bool prop);
 expr mk_nat();
 expr mk_nat_zero();
 expr mk_nat_one();
+expr mk_nat_bit0(expr const & e);
+expr mk_nat_bit1(expr const & e);
 expr mk_nat_add(expr const & e1, expr const & e2);
 
 bool is_ite(expr const & e, expr & c, expr & H, expr & A, expr & t, expr & f);
diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp
index a11b45ba08..50f8528fda 100644
--- a/src/library/vm/vm_expr.cpp
+++ b/src/library/vm/vm_expr.cpp
@@ -397,6 +397,10 @@ vm_obj vm_mk_string_val_ne_proof(vm_obj const & a, vm_obj const & b) {
     return to_obj(mk_string_val_ne_proof(to_expr(a), to_expr(b)));
 }
 
+vm_obj vm_mk_int_val_ne_proof(vm_obj const & a, vm_obj const & b) {
+    return to_obj(mk_int_val_ne_proof(to_expr(a), to_expr(b)));
+}
+
 void initialize_vm_expr() {
     DECLARE_VM_BUILTIN(name({"expr", "var"}),              expr_var);
     DECLARE_VM_BUILTIN(name({"expr", "sort"}),             expr_sort);
@@ -438,6 +442,7 @@ void initialize_vm_expr() {
     DECLARE_VM_BUILTIN(name("mk_fin_val_ne_proof"),        vm_mk_fin_val_ne_proof);
     DECLARE_VM_BUILTIN(name("mk_char_val_ne_proof"),       vm_mk_char_val_ne_proof);
     DECLARE_VM_BUILTIN(name("mk_string_val_ne_proof"),     vm_mk_string_val_ne_proof);
+    DECLARE_VM_BUILTIN(name("mk_int_val_ne_proof"),        vm_mk_int_val_ne_proof);
 
     // Not sure if we should expose these or what?
     DECLARE_VM_BUILTIN(name({"expr", "is_internal_cnstr"}), expr_is_internal_cnstr);
diff --git a/tests/lean/run/comp_val3.lean b/tests/lean/run/comp_val3.lean
new file mode 100644
index 0000000000..857a32d7f2
--- /dev/null
+++ b/tests/lean/run/comp_val3.lean
@@ -0,0 +1,52 @@
+open tactic
+
+example : (1:int) ≠ 2 :=
+by comp_val
+
+example : (1:int) ≠ 0 :=
+by comp_val
+
+example : (0:int) ≠ 1 :=
+by comp_val
+
+example : (3:int) ≠ 0 :=
+by comp_val
+
+example : (2:int) ≠ 1 :=
+by comp_val
+
+example : (3:int) ≠ -4 :=
+by comp_val
+
+example : (3:int) ≠ 4 :=
+by comp_val
+
+example : (100:int) ≠ 42919 :=
+by comp_val
+
+example : 42919 ≠ (100:int) :=
+by comp_val
+
+example : -(3:int) ≠ 49391 :=
+by comp_val
+
+example : -(3:int) ≠ 3 :=
+by comp_val
+
+example : -(100:int) ≠ -42919 :=
+by comp_val
+
+example : 0 ≠ -(1:int) :=
+by comp_val
+
+example : 0 ≠ -(100:int) :=
+by comp_val
+
+example : 0 ≠ -(2:int) :=
+by comp_val
+
+example : -(23:int) ≠ 0 :=
+by comp_val
+
+example : -(1 : int) ≠ 0 :=
+by comp_val