diff --git a/test-suite/bugs/bug_22093.v b/test-suite/bugs/bug_22093.v
new file mode 100644
index 0000000000..0750f1c972
--- /dev/null
+++ b/test-suite/bugs/bug_22093.v
@@ -0,0 +1,14 @@
+From Stdlib Require Import ZArith Lia.
+
+Section S.
+Open Scope Z_scope.
+Variable n : Z.
+Variable bound_n : 0 <= n < 1.
+
+Goal True.
+Proof.
+  Timeout 1 lia.
+  (* Used to not terminate, now 3ms *)
+Qed.
+
+End S.
diff --git a/theories/omega/PreOmega.v b/theories/omega/PreOmega.v
index db05110d12..2afd6c4681 100644
--- a/theories/omega/PreOmega.v
+++ b/theories/omega/PreOmega.v
@@ -99,7 +99,7 @@ Module Z.
   Ltac euclidean_division_equations_cleanup :=
     repeat
       (repeat match goal with
-         | [ H : 0 <= ?x < _ |- _ ] => destruct H
+         | [ H : 0 <= ?x < _ |- _ ] => tryif is_section_var H then destruct H; clear H else destruct H
          end;
        repeat match goal with
          | [ H : ?x <> ?x -> _ |- _ ] => clear H