diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean
index 66f4fb084..ce1f099a7 100644
--- a/library/algebra/ordered_field.lean
+++ b/library/algebra/ordered_field.lean
@@ -311,7 +311,7 @@ section linear_ordered_field
 
   theorem add_self_div_two (a : A) : (a + a) / 2 = a :=
   symm (iff.mpr (!eq_div_iff_mul_eq (ne_of_gt (add_pos zero_lt_one zero_lt_one)))
-       (by rewrite [left_distrib, *mul_one]))
+       (by krewrite [left_distrib, *mul_one]))
 
   theorem two_ge_one : (2:A) ≥ 1 :=
   calc (2:A) = 1+1 : one_add_one_eq_two
diff --git a/library/init/logic.lean b/library/init/logic.lean
index 7be8f3fe8..e07f23248 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -124,7 +124,7 @@ attribute eq.symm [symm]
 
 /- ne -/
 
-definition ne {A : Type} (a b : A) := ¬(a = b)
+definition ne [reducible] {A : Type} (a b : A) := ¬(a = b)
 notation a ≠ b := ne a b
 
 namespace ne
diff --git a/tests/lean/run/blast13.lean b/tests/lean/run/blast13.lean
index 4e13accf5..26cd8bca3 100644
--- a/tests/lean/run/blast13.lean
+++ b/tests/lean/run/blast13.lean
@@ -9,3 +9,6 @@ by blast
 
 example (A : Type) (p : Prop) (a b c : A) : a = b → ¬ b = a → p :=
 by blast
+
+example (A : Type) (p : Prop) (a b c : A) : a = b → b ≠ a → p :=
+by blast