diff --git a/src/util/lp/nla_order_lemmas.cpp b/src/util/lp/nla_order_lemmas.cpp
index 374ccfb7a..fc98db373 100644
--- a/src/util/lp/nla_order_lemmas.cpp
+++ b/src/util/lp/nla_order_lemmas.cpp
@@ -168,7 +168,7 @@ void order::generate_mon_ol(const monomial& ac,
     add_empty_lemma();
     mk_ineq(c_sign, c, llc::LE);
     explain(c); // this explains c == +- d
-    negate_var_factor_relation(c_sign, a, d_sign, b);
+    mk_ineq(c_sign, a, -d_sign, b.var(), negate(ab_cmp));
     mk_ineq(ac.var(), rational(-1), var(bd), ab_cmp);
     explain(bd);
     explain(b);
@@ -263,14 +263,6 @@ void order::generate_ol(const monomial& ac,
     TRACE("nla_solver", _().print_lemma(tout););
 }
 
-
-void order::negate_var_factor_relation(const rational& a_sign, lpvar a, const rational& b_sign, const factor& b) {
-    rational b_fs = canonize_sign(b);
-    llc cmp = a_sign*val(a) < b_sign*val(b)? llc::GE : llc::LE;
-    mk_ineq(a_sign, a, - b_fs*b_sign, var(b), cmp);
-}
-
-
 bool order::order_lemma_on_ac_and_bc_and_factors(const monomial& ac,
                                                  const factor& a,
                                                  const factor& c,
diff --git a/src/util/lp/nla_order_lemmas.h b/src/util/lp/nla_order_lemmas.h
index 01ee92a59..df8c646e7 100644
--- a/src/util/lp/nla_order_lemmas.h
+++ b/src/util/lp/nla_order_lemmas.h
@@ -88,6 +88,5 @@ private:
                          const rational& d_sign,
                          lpvar d,
                          llc ab_cmp);
-    void negate_var_factor_relation(const rational& a_sign, lpvar a, const rational& b_sign, const factor& b);
 };
 }