diff --git a/theories/base.v b/theories/base.v
index 0e6fece31159b8d091f21082cb0d806b604ecc5e..26652e64458801c86d54256c0271da4611fdd828 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; inversion 1; reflexivity. Qed.
+
 Inductive TCDiag {A} (C : A → Prop) : A → A → Prop :=
   | TCDiag_diag x : C x → TCDiag C x x.
 Existing Class TCDiag.
@@ -1000,7 +1003,7 @@ Hint Mode UpClose - ! : typeclass_instances.
 Notation "↑ x" := (up_close x) (at level 20, format "↑ x").
 
 (** * Monadic operations *)
-(** We define operational type classes for the monadic operations bind, join 
+(** We define operational type classes for the monadic operations bind, join
 and fmap. We use these type classes merely for convenient overloading of
 notations and do not formalize any theory on monads (we do not even define a
 class with the monad laws). *)
@@ -1106,7 +1109,7 @@ Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [partial_alter f k m] should update the value at key [k] using the
 function [f], which is called with the original value at key [k] or [None]
-if [k] is not a member of [m]. The value at [k] should be deleted if [f] 
+if [k] is not a member of [m]. The value at [k] should be deleted if [f]
 yields [None]. *)
 Class PartialAlter (K A M : Type) :=
   partial_alter: (option A → option A) → K → M → M.
diff --git a/theories/list.v b/theories/list.v
index 4d70d994a406b51bb8db7693e88783d951f8058d..5ea7b5f8c9e0e2ecb85f70696e6eb916bdc1d4cf 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -401,7 +401,7 @@ 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] 
+(** [seqZ m n] generates the sequence [m], [m + 1], ..., [m + n - 1]
 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)).
@@ -629,6 +629,11 @@ 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)%nat → l !! i = Some x) → <[i:=x]>l = l.
+Proof.
+  revert i. induction l; intros [|i]; simpl; intros Heq; try done; simpl; f_equal; eauto with lia.
+  injection Heq; try lia. done.
+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.
 Lemma list_insert_ge l i x : length l ≤ i → <[i:=x]>l = l.
@@ -1162,6 +1167,15 @@ 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 : n ≤ i → drop n (<[i:=x]>l) = <[i - n := x]>(drop n l).
+Proof.
+  intros. apply list_eq. intros j. rewrite !lookup_drop.
+  destruct (decide (i < length l)%nat).
+  - destruct (decide (i = n + j)%nat) as [Hi|Hi]; subst.
+    + assert (n + j - n = j) as ->. lia. rewrite !list_lookup_insert; try done. rewrite drop_length. lia.
+    + rewrite !list_lookup_insert_ne; try done; try lia. by rewrite lookup_drop.
+  - rewrite !list_insert_ge; try lia. by rewrite lookup_drop. by rewrite drop_length; lia.
+Qed.
 Lemma drop_insert l n i x : i < n → drop n (<[i:=x]>l) = drop n l.
 Proof.
   intros. apply list_eq. intros j.
@@ -1258,6 +1272,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.
@@ -3174,6 +3190,83 @@ Section find.
     intros HPQ. induction l as [|x l IH]; simpl; [done|].
     by rewrite (decide_iff (P x) (Q x)), IH by done.
   Qed.
+
+  Lemma list_find_app l1 l2:
+    list_find P l1 = None → list_find P (l1 ++ l2) = prod_map (λ x, x + length l1)%nat id <$> list_find P l2.
+  Proof.
+    induction l1 as [|a l1 IH].
+    - intros ?; simpl. destruct (list_find P l2) as [[??] |]; try done; simpl. do 2 f_equal. lia.
+    - simpl. case_decide; try done. destruct (list_find P l1) eqn:?; try done. intros _.
+      rewrite IH by done. destruct (list_find P (l2)) as [[??] |]; try done; simpl. do 2 f_equal. lia.
+  Qed.
+
+  Lemma list_find_app_None_l l1 l2 :
+    list_find P (l1 ++ l2) = None → list_find P l1 = None.
+  Proof. intros [??]%list_find_None%Forall_app. by apply list_find_None. Qed.
+  Lemma list_find_app_None_r l1 l2 :
+    list_find P (l1 ++ l2) = None → list_find P l2 = None.
+  Proof. intros [??]%list_find_None%Forall_app. by apply list_find_None. Qed.
+
+  Lemma list_find_insert_Some_eq1 l i x x':
+    list_find P l = Some (i, x') → P x →
+    list_find P (<[i:=x]> l) = Some (i, x).
+  Proof.
+    intros [Hl [? ?]]%list_find_Some ?. apply list_find_Some.
+    split_and?; try done.
+    - by apply list_lookup_insert; eapply lookup_lt_Some.
+    - intros ??. rewrite list_lookup_insert_ne; naive_solver.
+  Qed.
+
+  Lemma list_find_insert_Some_ne1 l i i' x x':
+    list_find P l = Some (i', x') → ¬ P x → i ≠ i' →
+    list_find P (<[i:=x]> l) = Some (i', x').
+  Proof.
+    intros [Hl [? ?]]%list_find_Some ??. apply list_find_Some.
+    assert (i' < length l) as ?. by eapply lookup_lt_Some.
+    split_and?; try done.
+    - by rewrite list_lookup_insert_ne.
+    - intros j ?. destruct (decide (i = j)); subst.
+      + rewrite list_lookup_insert; naive_solver lia.
+      + rewrite list_lookup_insert_ne; naive_solver.
+  Qed.
+
+  Lemma list_find_insert_Some_ne_change2 l i i' x x':
+    list_find P (<[i:=x]>l) = Some (i', x') → ¬ P x → l !! i = Some x' → i < i' →
+    list_find P l = Some (i, x').
+  Proof.
+    intros [Hl [? Hj]]%list_find_Some ???.
+    pose proof Hl as Hl2. revert Hl2. intros Hl2%lookup_lt_Some. rewrite insert_length in Hl2.
+    destruct (decide (i = i')); subst. by rewrite list_lookup_insert in Hl; simplify_eq.
+    rewrite list_lookup_insert_ne in Hl; try done.
+    apply list_find_Some; split_and?; try done. intros j ?.
+    pose proof (Hj j) as [?[Hlk ?]]; try lia.
+    rewrite list_lookup_insert_ne in Hlk; naive_solver lia.
+  Qed.
+
+  Lemma list_find_insert_Some_ne_same2 l i i' x x' x'':
+    list_find P (<[i:=x]>l) = Some (i', x') → ¬ P x → l !! i = Some x'' → (i < i' → ¬ P x'') →
+    list_find P l = Some (i', x').
+  Proof.
+    intros [Hl [? Hj]]%list_find_Some ???.
+    pose proof Hl as Hl2. revert Hl2. intros Hl2%lookup_lt_Some. rewrite insert_length in Hl2.
+    destruct (decide (i = i')); subst. by rewrite list_lookup_insert in Hl; simplify_eq.
+    rewrite list_lookup_insert_ne in Hl; try done.
+    apply list_find_Some; split_and?; try done. intros j ?.
+    pose proof (Hj j) as [?[Hlk ?]]; try lia.
+    destruct (decide (j = i)); subst.
+    - rewrite list_lookup_insert in Hlk; naive_solver lia.
+    - rewrite list_lookup_insert_ne in Hlk; naive_solver lia.
+  Qed.
+
+  Lemma list_find_insert_Some_ne2 l i i' x x' x'':
+    list_find P (<[i:=x]>l) = Some (i', x') → ¬ P x → l !! i = Some x'' → (x'' = x' ∨ ¬ P x'') →
+    ∃ i'', list_find P l = Some (i'', x').
+  Proof.
+    intros ???[?|?]; subst. destruct (decide (i < i')).
+    1: by eexists _; eapply list_find_insert_Some_ne_change2.
+    all: by eexists _; eapply list_find_insert_Some_ne_same2.
+  Qed.
+
 End find.
 
 (** * Properties of the monadic operations *)
@@ -3829,6 +3922,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. by induction l as [|?? IH]; csimpl; try done; rewrite IH. 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 [|?? IH]; try done; simpl. rewrite IH. apply Hf. 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,
@@ -4144,7 +4243,7 @@ Section positives_flatten_unflatten.
       rewrite 2!(assoc_L (++)).
       reflexivity.
   Qed.
-  
+
   Lemma positives_unflatten_go_app p suffix xs acc :
     positives_unflatten_go (suffix ++ Preverse (Pdup p)) xs acc =
     positives_unflatten_go suffix xs (acc ++ p).
@@ -4161,7 +4260,7 @@ Section positives_flatten_unflatten.
       reflexivity.
     - reflexivity.
   Qed.
-  
+
   Lemma positives_unflatten_flatten_go suffix xs acc :
     positives_unflatten_go (suffix ++ positives_flatten_go xs 1) acc 1 =
     positives_unflatten_go suffix (xs ++ acc) 1.
@@ -4178,7 +4277,7 @@ Section positives_flatten_unflatten.
       rewrite (left_id_L 1 (++)).
       reflexivity.
   Qed.
-  
+
   Lemma positives_unflatten_flatten xs :
     positives_unflatten (positives_flatten xs) = Some xs.
   Proof.
@@ -4191,7 +4290,7 @@ Section positives_flatten_unflatten.
     rewrite (right_id_L [] (++)%list).
     reflexivity.
   Qed.
-  
+
   Lemma positives_flatten_app xs ys :
     positives_flatten (xs ++ ys) = positives_flatten xs ++ positives_flatten ys.
   Proof.
@@ -4205,7 +4304,7 @@ Section positives_flatten_unflatten.
       rewrite (assoc_L (++)).
       reflexivity.
   Qed.
-  
+
   Lemma positives_flatten_cons x xs :
     positives_flatten (x :: xs) = 1~1~0 ++ Preverse (Pdup x) ++ positives_flatten xs.
   Proof.
@@ -4214,7 +4313,7 @@ Section positives_flatten_unflatten.
     rewrite (assoc_L (++)).
     reflexivity.
   Qed.
-  
+
   Lemma positives_flatten_suffix (l k : list positive) :
     l `suffix_of` k → ∃ q, positives_flatten k = q ++ positives_flatten l.
   Proof.
@@ -4222,7 +4321,7 @@ Section positives_flatten_unflatten.
     exists (positives_flatten l').
     apply positives_flatten_app.
   Qed.
-  
+
   Lemma positives_flatten_suffix_eq p1 p2 (xs ys : list positive) :
     length xs = length ys →
     p1 ++ positives_flatten xs = p2 ++ positives_flatten ys →
diff --git a/theories/numbers.v b/theories/numbers.v
index 44d57e3f60e7a7b621e7c727cf6da4b1e43bea3d..a655ac9c09516ea94715dc65294e1f61d779c0c5 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -121,6 +121,9 @@ Definition max_list_with {A} (f : A → nat) : list A → nat :=
   end.
 Notation max_list := (max_list_with id).
 
+Lemma max_list_le_in 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.
 
@@ -213,7 +216,7 @@ Proof.
   - by rewrite Preverse_xO, Preverse_app, IH.
   - reflexivity.
 Qed.
-    
+
 Instance Preverse_inj : Inj (=) (=) Preverse.
 Proof.
   intros p q eq.
@@ -473,6 +476,19 @@ 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_almost_small a b c :
+  0 ≤ a → 0 ≤ b →
+  c ≤ (a + b) →
+  a < c → b < c →
+  (a + b) `mod` c = a + b - c.
+Proof.
+  intros.
+  rewrite Zmod_eq_full; try lia.
+  assert (((a + b) `div` c) = 1) as ->. 2: lia.
+  assert ((a + b) `div` c < 2) as ?. by apply Z.div_lt_upper_bound; lia.
+  assert (1 ≤ (a + b) `div` c) as ?. by apply Z.div_le_lower_bound; lia.
+    lia.
+Qed.
 
 Local Close Scope Z_scope.
 
@@ -571,7 +587,7 @@ Proof.
   by apply Qcplus_le_mono_l.
 Qed.
 Lemma Qcplus_nonneg_pos (x y : Qc) : 0 ≤ x → 0 < y → 0 < x + y.
-Proof. rewrite (Qcplus_comm x). auto using Qcplus_pos_nonneg. Qed. 
+Proof. rewrite (Qcplus_comm x). auto using Qcplus_pos_nonneg. Qed.
 Lemma Qcplus_pos_pos (x y : Qc) : 0 < x → 0 < y → 0 < x + y.
 Proof. auto using Qcplus_pos_nonneg, Qclt_le_weak. Qed.
 Lemma Qcplus_nonneg_nonneg (x y : Qc) : 0 ≤ x → 0 ≤ y → 0 ≤ x + y.
diff --git a/theories/sets.v b/theories/sets.v
index 3ecda91da667ad85456175b9391ee31c008a0ec0..ca00b2a237301d16b8c53b5f0e75d6649c03d667 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -564,7 +564,7 @@ Section semi_set.
     Lemma union_list_reverse_L Xs : ⋃ (reverse Xs) = ⋃ Xs.
     Proof. unfold_leibniz. apply union_list_reverse. Qed.
     Lemma empty_union_list_L Xs : ⋃ Xs = ∅ ↔ Forall (.= ∅) Xs.
-    Proof. unfold_leibniz. by rewrite empty_union_list. Qed. 
+    Proof. unfold_leibniz. by rewrite empty_union_list. Qed.
   End leibniz.
 
   Lemma not_elem_of_iff `{!RelDecision (∈@{C})} X Y x :
@@ -604,7 +604,7 @@ Section set.
 
   (** Intersection *)
   Lemma subseteq_intersection X Y : X ⊆ Y ↔ X ∩ Y ≡ X.
-  Proof. set_solver. Qed. 
+  Proof. set_solver. Qed.
   Lemma subseteq_intersection_1 X Y : X ⊆ Y → X ∩ Y ≡ X.
   Proof. apply subseteq_intersection. Qed.
   Lemma subseteq_intersection_2 X Y : X ∩ Y ≡ X → X ⊆ Y.
@@ -1031,9 +1031,7 @@ Section pred_finite_infinite.
   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 H%max_list_le_in; lia.
   Qed.
 
   Lemma pred_finite_le n : pred_finite (flip le n).