diff --git a/src/tests/interval/mpfp_interval.cpp b/src/tests/interval/mpfp_interval.cpp
index 40cd6dbad..f9d223d7b 100644
--- a/src/tests/interval/mpfp_interval.cpp
+++ b/src/tests/interval/mpfp_interval.cpp
@@ -142,8 +142,8 @@ static void mpfp_interval_inf1() {
     cout << i1 << " * " << ozero_pinf << " = " << i1 * ozero_pinf << endl;
     cout << i1 << " * " << czero_ninf << " = " << i1 * czero_ninf << endl;
     cout << i1 << " * " << czero_pinf << " = " << i1 * czero_pinf << endl;
-    lean_assert(i1 * ozero_ninf != ozero_ninf); lean_assert(ozero_ninf * i1 == ozero_ninf);
-    lean_assert(i1 * ozero_pinf != ozero_pinf); lean_assert(ozero_pinf * i1 == ozero_pinf);
+    lean_assert(i1 * ozero_ninf == ozero_ninf); lean_assert(ozero_ninf * i1 == ozero_ninf);
+    lean_assert(i1 * ozero_pinf == ozero_pinf); lean_assert(ozero_pinf * i1 == ozero_pinf);
     lean_assert(i1 * czero_ninf == czero_ninf); lean_assert(czero_ninf * i1 == czero_ninf);
     lean_assert(i1 * czero_pinf == czero_pinf); lean_assert(czero_pinf * i1 == czero_pinf);
 
diff --git a/src/util/numerics/mpq.h b/src/util/numerics/mpq.h
index 4621bafd3..ecd30ec2f 100644
--- a/src/util/numerics/mpq.h
+++ b/src/util/numerics/mpq.h
@@ -71,38 +71,47 @@ public:
     friend int cmp(mpq const & a, mpz const & b);
     friend int cmp(mpq const & a, unsigned b) { return mpq_cmp_ui(a.m_val, b, 1); }
     friend int cmp(mpq const & a, int b) { return mpq_cmp_si(a.m_val, b, 1); }
+    friend int cmp(mpq const & a, double b) { return a.get_double() - b; }
 
     friend bool operator<(mpq const & a, mpq const & b) { return cmp(a, b) < 0; }
     friend bool operator<(mpq const & a, mpz const & b) { return cmp(a, b) < 0; }
     friend bool operator<(mpq const & a, unsigned b) { return cmp(a, b) < 0; }
     friend bool operator<(mpq const & a, int b) { return cmp(a, b) < 0; }
+    friend bool operator<(mpq const & a, double b) { return cmp(a, b) < 0; }
     friend bool operator<(mpz const & a, mpq const & b) { return cmp(b, a) > 0; }
     friend bool operator<(unsigned a, mpq const & b) { return cmp(b, a) > 0; }
     friend bool operator<(int a, mpq const & b) { return cmp(b, a) > 0; }
+    friend bool operator<(double a, mpq const & b) { return cmp(b, a) > 0; }
 
     friend bool operator>(mpq const & a, mpq const & b) { return cmp(a, b) > 0; }
     friend bool operator>(mpq const & a, mpz const & b) { return cmp(a, b) > 0; }
     friend bool operator>(mpq const & a, unsigned b) { return cmp(a, b) > 0; }
     friend bool operator>(mpq const & a, int b) { return cmp(a, b) > 0; }
+    friend bool operator>(mpq const & a, double b) { return cmp(a, b) > 0; }
     friend bool operator>(mpz const & a, mpq const & b) { return cmp(b, a) < 0; }
     friend bool operator>(unsigned a, mpq const & b) { return cmp(b, a) < 0; }
     friend bool operator>(int a, mpq const & b) { return cmp(b, a) < 0; }
+    friend bool operator>(double a, mpq const & b) { return cmp(b, a) < 0; }
 
     friend bool operator<=(mpq const & a, mpq const & b) { return cmp(a, b) <= 0; }
     friend bool operator<=(mpq const & a, mpz const & b) { return cmp(a, b) <= 0; }
     friend bool operator<=(mpq const & a, unsigned b) { return cmp(a, b) <= 0; }
     friend bool operator<=(mpq const & a, int b) { return cmp(a, b) <= 0; }
+    friend bool operator<=(mpq const & a, double b) { return cmp(a, b) <= 0; }
     friend bool operator<=(mpz const & a, mpq const & b) { return cmp(b, a) >= 0; }
     friend bool operator<=(unsigned a, mpq const & b) { return cmp(b, a) >= 0; }
     friend bool operator<=(int a, mpq const & b) { return cmp(b, a) >= 0; }
+    friend bool operator<=(double a, mpq const & b) { return cmp(b, a) >= 0; }
 
     friend bool operator>=(mpq const & a, mpq const & b) { return cmp(a, b) >= 0; }
     friend bool operator>=(mpq const & a, mpz const & b) { return cmp(a, b) >= 0; }
     friend bool operator>=(mpq const & a, unsigned b) { return cmp(a, b) >= 0; }
     friend bool operator>=(mpq const & a, int b) { return cmp(a, b) >= 0; }
+    friend bool operator>=(mpq const & a, double b) { return cmp(a, b) >= 0; }
     friend bool operator>=(mpz const & a, mpq const & b) { return cmp(b, a) <= 0; }
     friend bool operator>=(unsigned a, mpq const & b) { return cmp(b, a) <= 0; }
     friend bool operator>=(int a, mpq const & b) { return cmp(b, a) <= 0; }
+    friend bool operator>=(double a, mpq const & b) { return cmp(b, a) <= 0; }
 
     friend bool operator==(mpq const & a, mpq const & b) { return mpq_equal(a.m_val, b.m_val) != 0; }
     friend bool operator==(mpq const & a, mpz const & b) { return a.is_integer() && mpz_cmp(mpq_numref(a.m_val), zval(b)) == 0; }