diff --git a/src/util/lp/niil_solver.cpp b/src/util/lp/niil_solver.cpp
index 0503b7d46..6b1789857 100644
--- a/src/util/lp/niil_solver.cpp
+++ b/src/util/lp/niil_solver.cpp
@@ -864,8 +864,8 @@ struct solver::imp {
         return false;
     }
 
-    bool generate_basic_lemma_for_mon_proportionality(unsigned i_mon) {
-        TRACE("niil_solver", tout << "generate_basic_lemma_for_mon_proportionality";);
+    // we derive a lemma from |x| >= 1 => |xy| >= |y|
+    bool large_basic_lemma_for_mon_proportionality_from_factors_to_product(unsigned i_mon) {
         const mon_eq & m = m_monomials[i_mon];
         svector<unsigned> large;
         svector<unsigned> _small;
@@ -884,7 +884,19 @@ struct solver::imp {
             return true;
 
         return false;
+    }
 
+    bool generate_basic_lemma_for_mon_proportionality(unsigned i_mon) {
+        TRACE("niil_solver", tout << "generate_basic_lemma_for_mon_proportionality";);
+        if (large_basic_lemma_for_mon_proportionality_from_factors_to_product(i_mon))
+            return true;
+
+        return large_basic_lemma_for_mon_proportionality_from_product_to_factors(i_mon);
+    }
+    // we derive a lemma from |xy| > |y| => |x| >= 1 || |y| = 0
+    bool large_basic_lemma_for_mon_proportionality_from_product_to_factors(unsigned i_mon) {
+        SASSERT(false);
+        return false;
     }
 
     bool generate_basic_lemma_for_mon(unsigned i_mon) {