diff --git a/src/util/debug.h b/src/util/debug.h
index 8929df5dc..fa4d1bbde 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -85,6 +85,7 @@ Author: Leonardo de Moura
 #define lean_cond_assert(TAG, COND, ARGS...) DEBUG_CODE({if (lean::is_debug_enabled(TAG) && !(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(ARGS); lean::invoke_debugger(); }})
 
 #define lean_assert_eq(A, B) lean_assert(A == B, A, B)
+#define lean_assert_ne(A, B) lean_assert(A != B, A, B)
 #define lean_assert_gt(A, B) lean_assert(A > B, A, B)
 #define lean_assert_lt(A, B) lean_assert(A < B, A, B)
 #define lean_assert_ge(A, B) lean_assert(A >= B, A, B)