diff --git a/theories/list.v b/theories/list.v
index dd78fd26f51275ce789ffda381cd4607a154914f..a3d8b7076ef5a214593fc484c91a2ba9572d25a9 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3351,12 +3351,10 @@ Section seqZ.
Proof. by destruct n. Qed.
Lemma seqZ_cons m n: n > 0 → seqZ m n = m :: seqZ (Z.succ m) (Z.pred n).
Proof.
- intros H. unfold seqZ.
- replace (Z.to_nat n) with (S (Z.to_nat (n - 1))) by
- (rewrite <-Z2Nat.inj_succ; [f_equal|]; lia).
- simpl; f_equal.
- erewrite <-fmap_seq, map_map, map_ext; eauto.
- intros; lia.
+ intros H. unfold seqZ. replace n with (Z.succ (Z.pred n)) at 1 by lia.
+ rewrite Z2Nat.inj_succ by lia. f_equal/=.
+ rewrite <-fmap_seq, <-list_fmap_compose.
+ apply map_ext; naive_solver lia.
Qed.
Lemma seqZ_length m n: length (seqZ m n) = Z.to_nat n.
Proof. unfold seqZ; by rewrite fmap_length, seq_length. Qed.