diff --git a/library/algebra/simplifier.lean b/library/algebra/simplifier.lean
index 7005d17583..cd334e073c 100644
--- a/library/algebra/simplifier.lean
+++ b/library/algebra/simplifier.lean
@@ -18,6 +18,17 @@ namespace neg_helper
     lemma sub_def : a - b = a + (- b) := rfl
 end neg_helper
 
+namespace unit
+attribute algebra.zero_add [simp]
+attribute algebra.add_zero [simp]
+
+attribute algebra.zero_mul [simp]
+attribute algebra.mul_zero [simp]
+
+attribute algebra.one_mul [simp]
+attribute algebra.mul_one [simp]
+end unit
+
 namespace ac
 
 -- iff
diff --git a/src/library/blast/simplifier.cpp b/src/library/blast/simplifier.cpp
index 7098c44ef8..3405aab83a 100644
--- a/src/library/blast/simplifier.cpp
+++ b/src/library/blast/simplifier.cpp
@@ -522,18 +522,14 @@ result simplifier::simplify_fun(expr const & e) {
 }
 
 optional<result> simplifier::simplify_numeral(expr const & e) {
-    if (is_num(e)) {
-        return optional<result>(result(e));
-    } else if (is_add_app(e) || is_mul_app(e)) {
-        buffer<expr> args;
-        get_app_args(e, args);
-        if (is_num(args[2]) && is_num(args[3])){
-            expr_pair r = mk_norm_num(*m_tmp_tctx, e);
-            return optional<result>(result(r.first, r.second));
-        }
+    if (is_num(e)) { return optional<result>(result(e)); }
+
+    try {
+        expr_pair r = mk_norm_num(*m_tmp_tctx, e);
+        return optional<result>(result(r.first, r.second));
+    } catch (exception e) {
+        return optional<result>();
     }
-    // TODO(dhs): simplify division and substraction as well
-    return optional<result>();
 }
 
 /* Proving */
@@ -976,6 +972,7 @@ result simplifier::fuse(expr const & e) {
     }
 
     /* Prove (1) == (3) using simplify with [ac] */
+    flet<bool> no_simplify_numerals(m_numerals, false);
     auto pf_1_3 = prove(m_app_builder.mk_eq(e, e_grp),
                         get_simp_rule_sets(env(), ios(), *g_simplify_ac_namespace));
     if (!pf_1_3) {
@@ -992,8 +989,8 @@ result simplifier::fuse(expr const & e) {
     }
 
     /* Prove (5) == (6) using simplify with [numeral] */
-    result r_simp_ls = simplify(e_fused_ls,
-                                get_simp_rule_sets(env(), ios(), *g_simplify_numeral_namespace));
+    flet<bool> simplify_numerals(m_numerals, true);
+    result r_simp_ls = simplify(e_fused_ls, get_simp_rule_sets(env(), ios(), *g_simplify_unit_namespace));
 
     /* Prove (4) == (6) by transitivity of proofs (2) and (3) */
     expr pf_4_6;
diff --git a/tests/lean/simplifier14.lean b/tests/lean/simplifier14.lean
index c61f172dc2..40d7101fd2 100644
--- a/tests/lean/simplifier14.lean
+++ b/tests/lean/simplifier14.lean
@@ -6,7 +6,7 @@ universe l
 constants (T : Type.{l}) (s : algebra.comm_ring T)
 constants (x1 x2 x3 x4 : T) (f g : T → T)
 attribute s [instance]
-set_option simplify.max_steps 10000
+set_option simplify.max_steps 50000
 set_option simplify.fuse true
 
 #simplify eq simplifier.som 0 x1
@@ -26,4 +26,4 @@ set_option simplify.fuse true
 #simplify eq simplifier.som 0 x2 * x1 + 3 * x1 + (2 * x2 - 8 * x2 * 4 * x1) + x1 * x2
 #simplify eq simplifier.som 0 (x1 - 2 * x3 * x2) + x2 * x3 * 3 - 1 * 0 * x1 * x2
 #simplify eq simplifier.som 0 (x1 * x3 + x1 * 2 + x2 * 3 * x3 + x1 * x2) - 2* x2 * x1 + 1 * x2 * x1 - 3 * x1 * x3
-#simplify eq simplifier.som 0 x2 + x1 - x2 - - x1
+#simplify eq simplifier.som 0 x2 + x1 - x2 - (- x1)