diff --git a/stdpp/list.v b/stdpp/list.v
index 079a8133941d6a46e14c5d6e5e34bc662ea880ef..12db6e64352f540754b72d860d70af97521bd2c0 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -2135,6 +2135,12 @@ Proof. rewrite <-(take_drop n l) at 2. apply prefix_app_r. done. Qed.
 Lemma prefix_lookup l1 l2 i x :
   l1 !! i = Some x → l1 `prefix_of` l2 → l2 !! i = Some x.
 Proof. intros ? [k ->]. rewrite lookup_app_l; eauto using lookup_lt_Some. Qed.
+Lemma prefix_lookup_lt l1 l2 i :
+  i < length l1 → l1 `prefix_of` l2 → l1 !! i = l2 !! i.
+Proof.
+  intros Hlt Hprefix. apply lookup_lt_is_Some_2 in Hlt as [? Hlookup].
+  rewrite Hlookup. eapply prefix_lookup in Hlookup; eauto.
+Qed.
 Lemma prefix_length l1 l2 : l1 `prefix_of` l2 → length l1 ≤ length l2.
 Proof. intros [? ->]. rewrite app_length. lia. Qed.
 Lemma prefix_snoc_not l x : ¬l ++ [x] `prefix_of` l.
@@ -2181,6 +2187,18 @@ Proof.
   apply not_elem_of_app_cons_inv_l in Hle; [|done..]. unfold prefix. naive_solver.
 Qed.
 
+Lemma list_prefix_eq l1 l2 :
+  l1 `prefix_of` l2 → length l2 ≤ length l1 → l1 = l2.
+Proof.
+  intros Hprefix Hlen.
+  assert (length l1 = length l2).
+  { apply prefix_length in Hprefix; lia. }
+  eapply list_eq_same_length; [ done | done | ].
+  intros i x y ? Hlookup1 Hlookup2.
+  eapply prefix_lookup in Hlookup1; eauto.
+  congruence.
+Qed.
+
 Section prefix_ops.
   Context `{!EqDecision A}.
   Lemma max_prefix_fst l1 l2 :
diff --git a/stdpp/list_numbers.v b/stdpp/list_numbers.v
index 4d347802c551dc5144dca4fd5ec1916bfa8f35da..aea79e12632eaa5204dc94bdb03ccf343e90aad8 100644
--- a/stdpp/list_numbers.v
+++ b/stdpp/list_numbers.v
@@ -87,12 +87,6 @@ Section seq.
   Qed.
   Lemma NoDup_seq j n : NoDup (seq j n).
   Proof. apply NoDup_ListNoDup, seq_NoDup. Qed.
-  (* FIXME: This lemma is in the stdlib since Coq 8.12 *)
-  Lemma seq_S n j : seq j (S n) = seq j n ++ [j + n].
-  Proof.
-    revert j. induction n as [|n IH]; intros j; f_equal/=; [done |].
-    by rewrite IH, Nat.add_succ_r.
-  Qed.
 
   Lemma elem_of_seq j n k :
     k ∈ seq j n ↔ j ≤ k < j + n.
@@ -101,6 +95,24 @@ Section seq.
   Lemma Forall_seq (P : nat → Prop) i n :
     Forall P (seq i n) ↔ ∀ j, i ≤ j < i + n → P j.
   Proof. rewrite Forall_forall. setoid_rewrite elem_of_seq. auto with lia. Qed.
+
+  Lemma drop_seq j n m :
+    drop m (seq j n) = seq (j + m) (n - m).
+  Proof.
+    revert j m. induction n as [|n IH]; simpl; intros j m.
+    - rewrite drop_nil. done.
+    - destruct m; simpl.
+      + rewrite Nat.add_0_r. done.
+      + rewrite IH. f_equal; lia.
+  Qed.
+  Lemma take_seq j n m :
+    take m (seq j n) = seq j (m `min` n).
+  Proof.
+    revert j m. induction n as [|n IH]; simpl; intros j m.
+    - rewrite take_nil. replace (m `min` 0) with 0 by lia. done.
+    - destruct m; simpl. 1:done.
+      rewrite IH. done.
+  Qed.
 End seq.
 
 (** ** Properties of the [seqZ] function *)