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..4a4f2c0e9b 100644
--- a/theories/omega/PreOmega.v
+++ b/theories/omega/PreOmega.v
@@ -99,7 +99,12 @@ Module Z.
   Ltac euclidean_division_equations_cleanup :=
     repeat
       (repeat match goal with
-         | [ H : 0 <= ?x < _ |- _ ] => destruct H
+         | [ H : 0 <= ?x < _ |- _ ] =>
+            destruct H;
+            try (lazymatch type of H with (* matching on the type of H *after* the destruct, if H still present *)
+              | 0 <= x < _ => clear H (* H was a section variable, destruct didn't clear it, which would lead to an infinite loop *)
+            end)
+            (* tryif is_section_var H then destruct H; clear H else destruct H (* Cleaner version for Rocq >= 9.3 *) *)
          end;
        repeat match goal with
          | [ H : ?x <> ?x -> _ |- _ ] => clear H