diff --git a/theories/list.v b/theories/list.v
index a77fca1a5d66a7fce961e0f71b3159b98eb50bf8..8c50591c6392c199109874aaecaaee6ca712acef 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -401,9 +401,8 @@ used by [positives_flatten]. *)
 Definition positives_unflatten (p : positive) : option (list positive) :=
   positives_unflatten_go p [] 1.
 
-
 (** [seqZ m n] generates the sequence [m], [m + 1], ..., [m + n - 1] 
-over integers, provided [n >= 0]. If n < 0, then the range is empty. **)
+over integers, provided [0 ≤ n]. If [n < 0], then the range is empty. **)
 Definition seqZ (m len: Z) : list Z :=
   (λ i: nat, Z.add i m) <$> (seq 0 (Z.to_nat len)).
 Arguments seqZ : simpl never.