From ffffabad95bb7ce150d2a4436a4cd79d1b53cb79 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 14 Nov 2014 14:20:35 -0800
Subject: [PATCH] feat(kernel/level): improve is_geq procedure for universe
 levels

Now, it also returns true for

          (succ^k1 a)  =?=  k2

where k1 >= k2
---
 src/kernel/level.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index 21c864871..645e26f17 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -695,7 +695,7 @@ bool is_geq_core(level l1, level l2) {
         return is_geq(imax_rhs(l1), l2);
     auto p1 = to_offset(l1);
     auto p2 = to_offset(l2);
-    if (p1.first == p2.first)
+    if (p1.first == p2.first || is_zero(p2.first))
         return p1.second >= p2.second;
     if (p1.second == p2.second && p1.second > 0)
         return is_geq(p1.first, p2.first);