diff --git a/theories/list.v b/theories/list.v
index a3d8b7076ef5a214593fc484c91a2ba9572d25a9..394d7041273810986e34bc3a170dea578fa1d2c3 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3349,7 +3349,7 @@ Section seqZ.
Local Open Scope Z.
Lemma seqZ_nil m n: n ≤ 0 → seqZ m n = [].
Proof. by destruct n. Qed.
- Lemma seqZ_cons m n: n > 0 → seqZ m n = m :: seqZ (Z.succ m) (Z.pred n).
+ Lemma seqZ_cons m n: 0 < n → seqZ m n = m :: seqZ (Z.succ m) (Z.pred n).
Proof.
intros H. unfold seqZ. replace n with (Z.succ (Z.pred n)) at 1 by lia.
rewrite Z2Nat.inj_succ by lia. f_equal/=.