1 files changed, 1 insertions, 5 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 30cb38857..939ada461 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -767,11 +767,7 @@ Module Z.
     | _ => let LHS := match goal with |- ?LHS <= ?RHS => LHS end in
            match LHS with
            | context G[?x * (?y / ?z)]
-             => lazymatch x with
-                | context[_ / _] => fail
-                | _ => idtac
-                end;
-                let G' := context G[(x * y) / z] in
+             => let G' := context G[(x * y) / z] in
                 transitivity G'
            end
     end.