lt vs gt

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/=.