diff --git a/CHANGELOG.md b/CHANGELOG.md
index a14fe480c4b6aab7db02660f236744a75b7ee3dc..c98034737d21586c43de135c22bf51c3df4c8098 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,10 @@
 This file lists "large-ish" changes to the std++ Coq library, but not every
 API-breaking change is listed.
 
+## std++ master
+
+- Rename `drop_length` into `drop_length_gt` and add `drop_length_le`.
+
 ## std++ 1.3 (released 2020-03-18)
 
 Coq 8.11 is supported by this release.
diff --git a/theories/base.v b/theories/base.v
index c972c3f2ac04afd33e0740d31932fc87fea761b1..b76f16a28083e3f570ddf870af8cba9e33fa557b 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -153,6 +153,9 @@ Existing Class TCEq.
 Existing Instance TCEq_refl.
 Hint Mode TCEq ! - - : typeclass_instances.
 
+Lemma TCEq_eq {A} (x1 x2 : A) : TCEq x1 x2 ↔ x1 = x2.
+Proof. split; destruct 1; reflexivity. Qed.
+
 Inductive TCDiag {A} (C : A → Prop) : A → A → Prop :=
   | TCDiag_diag x : C x → TCDiag C x x.
 Existing Class TCDiag.
diff --git a/theories/list.v b/theories/list.v
index 0cb74cf52961b9585c90c539d38886b757790380..1203a5db8a9052755862aa9ff5f4e8e283787e9e 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -629,8 +629,10 @@ Qed.
 Lemma list_insert_commute l i j x y :
   i ≠ j → <[i:=x]>(<[j:=y]>l) = <[j:=y]>(<[i:=x]>l).
 Proof. revert i j. by induction l; intros [|?] [|?] ?; f_equal/=; auto. Qed.
+Lemma list_insert_id' l i x : (i < length l → l !! i = Some x) → <[i:=x]>l = l.
+Proof. revert i. induction l; intros [|i] ?; f_equal/=; naive_solver lia. Qed.
 Lemma list_insert_id l i x : l !! i = Some x → <[i:=x]>l = l.
-Proof. revert i. induction l; intros [|i] [=]; f_equal/=; auto. Qed.
+Proof. intros ?. by apply list_insert_id'. Qed.
 Lemma list_insert_ge l i x : length l ≤ i → <[i:=x]>l = l.
 Proof. revert i. induction l; intros [|i] ?; f_equal/=; auto with lia. Qed.
 Lemma list_insert_insert l i x y : <[i:=x]> (<[i:=y]> l) = <[i:=x]> l.
@@ -1162,7 +1164,9 @@ Proof.
   intros. apply list_eq. intros j.
   by rewrite !lookup_drop, !list_lookup_alter_ne by lia.
 Qed.
-Lemma drop_insert l n i x : i < n → drop n (<[i:=x]>l) = drop n l.
+Lemma drop_insert_le l n i x : n ≤ i → drop n (<[i:=x]>l) = <[i-n:=x]>(drop n l).
+Proof. revert i n. induction l; intros [] []; naive_solver lia. Qed.
+Lemma drop_insert_gt l n i x : i < n → drop n (<[i:=x]>l) = drop n l.
 Proof.
   intros. apply list_eq. intros j.
   by rewrite !lookup_drop, !list_lookup_insert_ne by lia.
@@ -1258,6 +1262,8 @@ Proof.
 Qed.
 Lemma replicate_false βs n : length βs = n → replicate n false =.>* βs.
 Proof. intros <-. by induction βs; simpl; constructor. Qed.
+Lemma tail_replicate x n : tail (replicate n x) = replicate (pred n) x.
+Proof. by destruct n. Qed.
 
 (** ** Properties of the [resize] function *)
 Lemma resize_spec l n x : resize n x l = take n l ++ replicate (n - length l) x.
@@ -3631,7 +3637,7 @@ Section seq.
   Qed.
   Lemma imap_seq_0 {A} (l : list A) (g : nat → A) :
     imap (λ j _, g j) l = g <$> seq 0 (length l).
-  Proof. rewrite (imap_ext _ (λ i o, g (0 + i))%nat); [|done]. apply imap_seq. Qed.
+  Proof. rewrite (imap_ext _ (λ i o, g (0 + i))); [|done]. apply imap_seq. Qed.
   Lemma lookup_seq_lt j n i : i < n → seq j n !! i = Some (j + i).
   Proof.
     revert j i. induction n as [|n IH]; intros j [|i] ?; simpl; auto with lia.
@@ -3829,6 +3835,12 @@ Definition foldr_app := @fold_right_app.
 Lemma foldl_app {A B} (f : A → B → A) (l k : list B) (a : A) :
   foldl f a (l ++ k) = foldl f (foldl f a l) k.
 Proof. revert a. induction l; simpl; auto. Qed.
+Lemma foldr_fmap {A B C} (f : B → A → A) x (l : list C) g :
+  foldr f x (g <$> l) = foldr (λ b a, f (g b) a) x l.
+Proof. induction l; f_equal/=; auto. Qed.
+Lemma foldr_ext {A B} (f1 f2 : B → A → A) x1 x2 l1 l2 :
+  (∀ b a, f1 b a = f2 b a) → l1 = l2 → x1 = x2 → foldr f1 x1 l1 = foldr f2 x2 l2.
+Proof. intros Hf -> ->. induction l2 as [|x l2 IH]; f_equal/=; by rewrite Hf, IH. Qed.
 Lemma foldr_permutation {A B} (R : relation B) `{!PreOrder R}
     (f : A → B → B) (b : B) `{Hf : !∀ x, Proper (R ==> R) (f x)} (l1 l2 : list A) :
   (∀ j1 a1 j2 a2 b,
diff --git a/theories/numbers.v b/theories/numbers.v
index 330dcf47080ce9c2e002c8cab26441611ff6fb04..8f2914358c461010faf97feafd6269fdc4c9c3a1 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -121,6 +121,10 @@ Definition max_list_with {A} (f : A → nat) : list A → nat :=
   end.
 Notation max_list := (max_list_with id).
 
+Lemma max_list_elem_of_le n ns:
+  n ∈ ns → (n ≤ max_list ns)%nat.
+Proof. induction 1; simpl; lia. Qed.
+
 (** * Notations and properties of [positive] *)
 Local Open Scope positive_scope.
 
@@ -473,6 +477,10 @@ Lemma Z_succ_pred_induction y (P : Z → Prop) :
   (∀ x, x ≤ y → P x → P (Z.pred x)) →
   (∀ x, P x).
 Proof. intros H0 HS HP. by apply (Z.order_induction' _ _ y). Qed.
+Lemma Zmod_in_range q a c :
+  q * c ≤ a < (q + 1) * c →
+  a `mod` c = a - q * c.
+Proof. intros ?. symmetry. apply Z.mod_unique_pos with q; lia. Qed.
 
 Local Close Scope Z_scope.
 
diff --git a/theories/sets.v b/theories/sets.v
index 5e63b40a023026af7934f06128946201db147e27..33fee8f5405e82b5cd8503ee0211ee8a44094529 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -1029,11 +1029,8 @@ Section pred_finite_infinite.
   Qed.
   Lemma pred_infinite_lt n : pred_infinite (lt n).
   Proof.
-    intros l. exists (S (n `max` max_list l)). split.
-    - induction l; simpl; lia.
-    - assert (∀ n, n ∈ l → n ≤ max_list l) as help.
-      { induction 1; simpl; lia. }
-      intros H%help; lia.
+    intros l. exists (S (n `max` max_list l)). split; [lia| ].
+    intros H%max_list_elem_of_le; lia.
   Qed.
 
   Lemma pred_finite_le n : pred_finite (flip le n).