diff --git a/CHANGELOG.md b/CHANGELOG.md
index a64d01b15a0603f39a3b2415689195995011da6e..26c7615cc15b0d647e82c76028966c01ce03d82f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -44,6 +44,15 @@ Coq 8.11 is no longer supported.
 - Change `list_fmap_ext` and `list_fmap_equiv_ext` to require equality on the
   elements of the list, not on all elements of the carrier type. This change
   makes these lemmas consistent with those for maps.
+- Use the modules `Nat`, `Pos`, `N`, `Z`, `Nat2Z`, `Z2Nat`, `Nat2N`, `Pos2Nat`,
+  `SuccNat2Pos`, and `N2Z` for our extended results on number types. Before,
+  we prefixed our the std++ lemmas with `Nat_` or `nat_`, but now you refer
+  to them with `Nat.`, similar to the way you refer to number lemmas from Coq's
+  standard library.
+- Use a module `Qp` for our positive rationals library. You now refer to `Qp`
+  lemmas using `Qp.lem` instead of `Qp_lem`.
+- Rename `_plus`/`_minus` into `_add`/`_sub` to be consistent with Coq's current
+  convention for numbers. See the sed script below for an exact list of renames.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
@@ -53,6 +62,47 @@ sed -i -E -f- $(find theories -name "*.v") <<EOF
 s/\bmap_disjoint_subseteq\b/kmap_subseteq/g
 s/\bmap_disjoint_subset\b/kmap_subset/g
 s/\blookup_union_l\b/lookup_union_l'/g
+# number modules --- note that this might rename your own lemmas
+# start with Nat_/N_/Z_/Qp_/P(app|reverse|length|dup)_ too eagerly.
+s/\bNat_/Nat\./g
+s/\bNat.iter_S(|_r)\b/Nat.iter_succ\1/g
+s/\bP(app|reverse|length|dup)/Pos\.\1/g
+s/\bPlt_sum\b/Pos\.lt_sum/g
+s/\bPos\.reverse_Pdup\b/Pos\.reverse_Pdup/g
+s/\bnat_le_sum\b/Nat\.le_sum/g
+s/\bN_/N\./g
+s/\bZ_/Z\./g
+s/\bZ\.scope\b/Z_scope/g
+s/\bN\.scope\b/N_scope/g
+s/\Z\.of_nat_complete\b/Z_of_nat_complete/g
+s/\bZ\.of_nat_inj\b/Nat2Z.inj/g
+s/\bZ2Nat_/Z2Nat\./g
+s/\bNat2Z_/Nat2Z\./g
+s/\bQp_/Qp\./g
+s/\bQp\.1_1/Qp\.add_1_1/g
+# plus → add
+s/\bfin_plus_inv\b/fin_add_inv/g
+s/\bfin_plus_inv_L\b/fin_add_inv_l/g
+s/\bfin_plus_inv_R\b/fin_add_inv_r/g
+s/\bset_seq_plus\b/set_seq_add/g
+s/\bset_seq_plus_L\b/set_seq_add_L/g
+s/\bset_seq_plus_disjoint\b/set_seq_add_disjoint/g
+s/\bnsteps_plus_inv\b/nsteps_add_inv/g
+s/\bbsteps_plus_r\b/bsteps_add_r/g
+s/\bbsteps_plus_l\b/bsteps_add_l/g
+s/\btake_plus_app\b/take_add_app/g
+s/\breplicate_plus\b/replicate_add/g
+s/\btake_replicate_plus\b/take_replicate_add/g
+s/\bdrop_replicate_plus\b/drop_replicate_add/g
+s/\bresize_plus\b/resize_add/g
+s/\bresize_plus_eq\b/resize_add_eq/g
+s/\btake_resize_plus\b/take_resize_add/g
+s/\bdrop_resize_plus\b/drop_resize_add/g
+s/\bdrop_plus_app\b/drop_add_app/g
+s/\bMakeNatPlus\b/MakeNatAdd/g
+s/\bmake_nat_plus\b/make_nat_add/g
+s/\bnat_minus_plus\b/Nat\.sub_add/g
+s/\bnat_le_plus_minus\b/Nat\.le_add_sub/g
 EOF
 ```
 
diff --git a/stdpp/countable.v b/stdpp/countable.v
index ad12a3daf2f98ceeb2ae098e499ad15e6d90dad5..7ced6edb32f73896fdec4492f8c52b837d5c6598 100644
--- a/stdpp/countable.v
+++ b/stdpp/countable.v
@@ -298,7 +298,7 @@ Global Program Instance Qp_countable : Countable Qp :=
     (λ p : Qc, guard (0 < p)%Qc as Hp; Some (mk_Qp p Hp)) _.
 Next Obligation.
   intros [p Hp]. unfold mguard, option_guard; simpl.
-  case_match; [|done]. f_equal. by apply Qp_to_Qc_inj_iff.
+  case_match; [|done]. f_equal. by apply Qp.to_Qc_inj_iff.
 Qed.
 
 Global Program Instance fin_countable n : Countable (fin n) :=
diff --git a/stdpp/fin.v b/stdpp/fin.v
index 0701c7a7aff7c8bb3c7a07d725705af94fa340ca..a3d6aa1cfadc419de0edb0b1cd5f01169556efe7 100644
--- a/stdpp/fin.v
+++ b/stdpp/fin.v
@@ -87,26 +87,26 @@ Qed.
 Lemma nat_to_fin_to_nat {n} (i : fin n) H : @nat_to_fin (fin_to_nat i) n H = i.
 Proof. apply (inj fin_to_nat), fin_to_nat_to_fin. Qed.
 
-Fixpoint fin_plus_inv {n1 n2} : ∀ (P : fin (n1 + n2) → Type)
+Fixpoint fin_add_inv {n1 n2} : ∀ (P : fin (n1 + n2) → Type)
     (H1 : ∀ i1 : fin n1, P (Fin.L n2 i1))
     (H2 : ∀ i2, P (Fin.R n1 i2)) (i : fin (n1 + n2)), P i :=
   match n1 with
   | 0 => λ P H1 H2 i, H2 i
-  | S n => λ P H1 H2, fin_S_inv P (H1 0%fin) (fin_plus_inv _ (λ i, H1 (FS i)) H2)
+  | S n => λ P H1 H2, fin_S_inv P (H1 0%fin) (fin_add_inv _ (λ i, H1 (FS i)) H2)
   end.
 
-Lemma fin_plus_inv_L {n1 n2} (P : fin (n1 + n2) → Type)
+Lemma fin_add_inv_l {n1 n2} (P : fin (n1 + n2) → Type)
     (H1: ∀ i1 : fin n1, P (Fin.L _ i1)) (H2: ∀ i2, P (Fin.R _ i2)) (i: fin n1) :
-  fin_plus_inv P H1 H2 (Fin.L n2 i) = H1 i.
+  fin_add_inv P H1 H2 (Fin.L n2 i) = H1 i.
 Proof.
   revert P H1 H2 i.
   induction n1 as [|n1 IH]; intros P H1 H2 i; inv_fin i; simpl; auto.
   intros i. apply (IH (λ i, P (FS i))).
 Qed.
 
-Lemma fin_plus_inv_R {n1 n2} (P : fin (n1 + n2) → Type)
+Lemma fin_add_inv_r {n1 n2} (P : fin (n1 + n2) → Type)
     (H1: ∀ i1 : fin n1, P (Fin.L _ i1)) (H2: ∀ i2, P (Fin.R _ i2)) (i: fin n2) :
-  fin_plus_inv P H1 H2 (Fin.R n1 i) = H2 i.
+  fin_add_inv P H1 H2 (Fin.R n1 i) = H2 i.
 Proof.
   revert P H1 H2 i; induction n1 as [|n1 IH]; intros P H1 H2 i; simpl; auto.
   apply (IH (λ i, P (FS i))).
diff --git a/stdpp/gmultiset.v b/stdpp/gmultiset.v
index dabfc11ff6c9a3177cf339a3385f88694c5aecc4..99af32e6496d2a41ef25930c3e5322573f385b73 100644
--- a/stdpp/gmultiset.v
+++ b/stdpp/gmultiset.v
@@ -438,7 +438,7 @@ Section more_lemmas.
         by (by rewrite ?lookup_union_with, ?lookup_delete, ?HX).
       rewrite (assoc_L _), <-(comm (++) (f (_,n'))), <-!(assoc_L _), <-IH.
       rewrite (assoc_L _). f_equiv.
-      rewrite (comm _); simpl. by rewrite replicate_plus, Permutation_middle.
+      rewrite (comm _); simpl. by rewrite replicate_add, Permutation_middle.
     - rewrite <-insert_union_with_l, !map_to_list_insert, !bind_cons
         by (by rewrite ?lookup_union_with, ?HX, ?HY).
       by rewrite <-(assoc_L (++)), <-IH.
diff --git a/stdpp/list.v b/stdpp/list.v
index 807dbc5b79b4a4ac28c43fc1d593b107c6162bae..9a084b617c7d01e30f821a4a52d746e089f89f9c 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -406,7 +406,7 @@ for example used for the countable instance of lists and in namespaces.
 Fixpoint positives_flatten_go (xs : list positive) (acc : positive) : positive :=
   match xs with
   | [] => acc
-  | x :: xs => positives_flatten_go xs (acc~1~0 ++ Preverse (Pdup x))
+  | x :: xs => positives_flatten_go xs (acc~1~0 ++ Pos.reverse (Pos.dup x))
   end.
 
 (** Flatten a list of positives into a single positive by duplicating the bits
@@ -1244,7 +1244,7 @@ Lemma take_app3_alt l1 l2 l3 n : n = length l1 → take n ((l1 ++ l2) ++ l3) = l
 Proof. intros ->. by rewrite <-(assoc_L (++)), take_app. Qed.
 Lemma take_app_le l k n : n ≤ length l → take n (l ++ k) = take n l.
 Proof. revert n. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
-Lemma take_plus_app l k n m :
+Lemma take_add_app l k n m :
   length l = n → take (n + m) (l ++ k) = l ++ take m k.
 Proof. intros <-. induction l; f_equal/=; auto. Qed.
 Lemma take_app_ge l k n :
@@ -1339,7 +1339,7 @@ Proof.
   intros. rewrite <-(Nat.sub_add (length l) n) at 1 by done.
   by rewrite Nat.add_comm, <-drop_drop, drop_app.
 Qed.
-Lemma drop_plus_app l k n m :
+Lemma drop_add_app l k n m :
   length l = n → drop (n + m) (l ++ k) = drop m k.
 Proof. intros <-. by rewrite <-drop_drop, drop_app. Qed.
 Lemma lookup_drop l n i : drop n l !! i = l !! (n + i).
@@ -1438,7 +1438,7 @@ Lemma replicate_S n x : replicate (S n) x = x :: replicate  n x.
 Proof. done. Qed.
 Lemma replicate_S_end n x : replicate (S n) x = replicate n x ++ [x].
 Proof. induction n; f_equal/=; auto. Qed.
-Lemma replicate_plus n m x :
+Lemma replicate_add n m x :
   replicate (n + m) x = replicate n x ++ replicate m x.
 Proof. induction n; f_equal/=; auto. Qed.
 Lemma replicate_cons_app n x :
@@ -1446,11 +1446,11 @@ Lemma replicate_cons_app n x :
 Proof. induction n; f_equal/=; eauto.  Qed.
 Lemma take_replicate n m x : take n (replicate m x) = replicate (min n m) x.
 Proof. revert m. by induction n; intros [|?]; f_equal/=. Qed.
-Lemma take_replicate_plus n m x : take n (replicate (n + m) x) = replicate n x.
+Lemma take_replicate_add n m x : take n (replicate (n + m) x) = replicate n x.
 Proof. by rewrite take_replicate, min_l by lia. Qed.
 Lemma drop_replicate n m x : drop n (replicate m x) = replicate (m - n) x.
 Proof. revert m. by induction n; intros [|?]; f_equal/=. Qed.
-Lemma drop_replicate_plus n m x : drop n (replicate (n + m) x) = replicate m x.
+Lemma drop_replicate_add n m x : drop n (replicate (n + m) x) = replicate m x.
 Proof. rewrite drop_replicate. f_equal. lia. Qed.
 Lemma replicate_as_elem_of x n l :
   replicate n x = l ↔ length l = n ∧ ∀ y, y ∈ l → y = x.
@@ -1490,16 +1490,16 @@ Lemma resize_all l x : resize (length l) x l = l.
 Proof. intros. by rewrite resize_le, take_ge. Qed.
 Lemma resize_all_alt l n x : n = length l → resize n x l = l.
 Proof. intros ->. by rewrite resize_all. Qed.
-Lemma resize_plus l n m x :
+Lemma resize_add l n m x :
   resize (n + m) x l = resize n x l ++ resize m x (drop n l).
 Proof.
   revert n m. induction l; intros [|?] [|?]; f_equal/=; auto.
   - by rewrite Nat.add_0_r, (right_id_L [] (++)).
-  - by rewrite replicate_plus.
+  - by rewrite replicate_add.
 Qed.
-Lemma resize_plus_eq l n m x :
+Lemma resize_add_eq l n m x :
   length l = n → resize (n + m) x l = l ++ replicate m x.
-Proof. intros <-. by rewrite resize_plus, resize_all, drop_all, resize_nil. Qed.
+Proof. intros <-. by rewrite resize_add, resize_all, drop_all, resize_nil. Qed.
 Lemma resize_app_le l1 l2 n x :
   n ≤ length l1 → resize n x (l1 ++ l2) = resize n x l1.
 Proof.
@@ -1537,7 +1537,7 @@ Lemma take_resize_le l n m x : n ≤ m → take n (resize m x l) = resize n x l.
 Proof. intros. by rewrite take_resize, Nat.min_l. Qed.
 Lemma take_resize_eq l n x : take n (resize n x l) = resize n x l.
 Proof. intros. by rewrite take_resize, Nat.min_l. Qed.
-Lemma take_resize_plus l n m x : take n (resize (n + m) x l) = resize n x l.
+Lemma take_resize_add l n m x : take n (resize (n + m) x l) = resize n x l.
 Proof. by rewrite take_resize, min_l by lia. Qed.
 Lemma drop_resize_le l n m x :
   n ≤ m → drop n (resize m x l) = resize (m - n) x (drop n l).
@@ -1546,7 +1546,7 @@ Proof.
   - intros. by rewrite drop_nil, !resize_nil, drop_replicate.
   - intros [|?] [|?] ?; simpl; try case_match; auto with lia.
 Qed.
-Lemma drop_resize_plus l n m x :
+Lemma drop_resize_add l n m x :
   drop n (resize (n + m) x l) = resize m x (drop n l).
 Proof. rewrite drop_resize_le by lia. f_equal. lia. Qed.
 Lemma lookup_resize l n x i : i < n → i < length l → resize n x l !! i = l !! i.
@@ -1578,7 +1578,7 @@ Proof. intros. by rewrite !list_lookup_total_alt, lookup_resize_old. Qed.
 Lemma rotate_replicate n1 n2 x:
   rotate n1 (replicate n2 x) = replicate n2 x.
 Proof.
-  unfold rotate. rewrite drop_replicate, take_replicate, <-replicate_plus.
+  unfold rotate. rewrite drop_replicate, take_replicate, <-replicate_add.
   f_equal. lia.
 Qed.
 
@@ -3355,7 +3355,7 @@ Section Forall2.
     { rewrite <-(resize_resize l m n) by done. by apply Forall2_resize. }
     intros. assert (n = length k); subst.
     { by rewrite <-(Forall2_length (resize n x l) k), resize_length. }
-    rewrite (nat_le_plus_minus (length k) m), !resize_plus,
+    rewrite (Nat.le_add_sub (length k) m), !resize_add,
       resize_all, drop_all, resize_nil by lia.
     auto using Forall2_app, Forall2_replicate_r,
       Forall_resize, Forall_drop, resize_length.
@@ -3368,7 +3368,7 @@ Section Forall2.
     { rewrite <-(resize_resize k m n) by done. by apply Forall2_resize. }
     assert (n = length l); subst.
     { by rewrite (Forall2_length l (resize n y k)), resize_length. }
-    rewrite (nat_le_plus_minus (length l) m), !resize_plus,
+    rewrite (Nat.le_add_sub (length l) m), !resize_add,
       resize_all, drop_all, resize_nil by lia.
     auto using Forall2_app, Forall2_replicate_l,
       Forall_resize, Forall_drop, resize_length.
@@ -3802,7 +3802,7 @@ Section find.
           naive_solver eauto using lookup_app_l_Some with lia. }
         apply list_find_Some. split_and!; [done..|].
         intros j z ??. eapply (Hleast (length l1 + j)); [|lia].
-        by rewrite lookup_app_r, nat_minus_plus by lia.
+        by rewrite lookup_app_r, Nat.sub_add' by lia.
     - intros [(?&?&Hleast)%list_find_Some|(?&Hl1&(?&?&Hleast)%list_find_Some)].
       + apply list_find_Some. split_and!; [by auto using lookup_app_l_Some..|].
         assert (i < length l1) by eauto using lookup_lt_Some.
@@ -4844,7 +4844,8 @@ Global Instance TCForall_app {A} (P : A → Prop) xs ys :
   TCForall P xs → TCForall P ys → TCForall P (xs ++ ys).
 Proof. rewrite !TCForall_Forall. apply Forall_app_2. Qed.
 
-Lemma TCForall2_Forall2 {A B} (P : A → B → Prop) xs ys : TCForall2 P xs ys ↔ Forall2 P xs ys.
+Lemma TCForall2_Forall2 {A B} (P : A → B → Prop) xs ys :
+  TCForall2 P xs ys ↔ Forall2 P xs ys.
 Proof. split; induction 1; constructor; auto. Qed.
 
 Lemma TCExists_Exists {A} (P : A → Prop) l : TCExists P l ↔ Exists P l.
@@ -4866,16 +4867,16 @@ Section positives_flatten_unflatten.
   Qed.
 
   Lemma positives_unflatten_go_app p suffix xs acc :
-    positives_unflatten_go (suffix ++ Preverse (Pdup p)) xs acc =
+    positives_unflatten_go (suffix ++ Pos.reverse (Pos.dup p)) xs acc =
     positives_unflatten_go suffix xs (acc ++ p).
   Proof.
     revert suffix acc.
     induction p as [p IH|p IH|]; intros acc suffix; simpl.
-    - rewrite 2!Preverse_xI.
+    - rewrite 2!Pos.reverse_xI.
       rewrite 2!(assoc_L (++)).
       rewrite IH.
       reflexivity.
-    - rewrite 2!Preverse_xO.
+    - rewrite 2!Pos.reverse_xO.
       rewrite 2!(assoc_L (++)).
       rewrite IH.
       reflexivity.
@@ -4927,7 +4928,8 @@ Section positives_flatten_unflatten.
   Qed.
 
   Lemma positives_flatten_cons x xs :
-    positives_flatten (x :: xs) = 1~1~0 ++ Preverse (Pdup x) ++ positives_flatten xs.
+    positives_flatten (x :: xs)
+    = 1~1~0 ++ Pos.reverse (Pos.dup x) ++ positives_flatten xs.
   Proof.
     change (x :: xs) with ([x] ++ xs)%list.
     rewrite positives_flatten_app.
@@ -4953,9 +4955,9 @@ Section positives_flatten_unflatten.
     rewrite !positives_flatten_cons, !(assoc _); intros Hl.
     assert (xs = ys) as <- by eauto; clear IH; f_equal.
     apply (inj (.++ positives_flatten xs)) in Hl.
-    rewrite 2!Preverse_Pdup in Hl.
-    apply (Pdup_suffix_eq _ _ p1 p2) in Hl.
-    by apply (inj Preverse).
+    rewrite 2!Pos.reverse_dup in Hl.
+    apply (Pos.dup_suffix_eq _ _ p1 p2) in Hl.
+    by apply (inj Pos.reverse).
   Qed.
 End positives_flatten_unflatten.
 
diff --git a/stdpp/list_numbers.v b/stdpp/list_numbers.v
index b85189c7891a193d1f2686e4bc8681e0c1a15d5b..4d347802c551dc5144dca4fd5ec1916bfa8f35da 100644
--- a/stdpp/list_numbers.v
+++ b/stdpp/list_numbers.v
@@ -121,7 +121,7 @@ Section seqZ.
   Proof. unfold seqZ; by rewrite fmap_length, seq_length. Qed.
   Lemma fmap_add_seqZ m m' n : Z.add m <$> seqZ m' n = seqZ (m + m') n.
   Proof.
-    revert m'. induction n as [|n ? IH|] using (Z_succ_pred_induction 0); intros m'.
+    revert m'. induction n as [|n ? IH|] using (Z.succ_pred_induction 0); intros m'.
     - by rewrite seqZ_nil.
     - rewrite (seqZ_cons m') by lia. rewrite (seqZ_cons (m + m')) by lia.
       f_equal/=. rewrite Z.pred_succ, IH; simpl. f_equal; lia.
@@ -129,7 +129,7 @@ Section seqZ.
   Qed.
   Lemma lookup_seqZ_lt m n i : Z.of_nat i < n → seqZ m n !! i = Some (m + Z.of_nat i).
   Proof.
-    revert m i. induction n as [|n ? IH|] using (Z_succ_pred_induction 0);
+    revert m i. induction n as [|n ? IH|] using (Z.succ_pred_induction 0);
       intros m i Hi; [lia| |lia].
     rewrite seqZ_cons by lia. destruct i as [|i]; simpl.
     - f_equal; lia.
@@ -140,7 +140,7 @@ Section seqZ.
   Lemma lookup_seqZ_ge m n i : n ≤ Z.of_nat i → seqZ m n !! i = None.
   Proof.
     revert m i.
-    induction n as [|n ? IH|] using (Z_succ_pred_induction 0); intros m i Hi; try lia.
+    induction n as [|n ? IH|] using (Z.succ_pred_induction 0); intros m i Hi; try lia.
     - by rewrite seqZ_nil.
     - rewrite seqZ_cons by lia.
       destruct i as [|i]; simpl; [lia|]. by rewrite Z.pred_succ, IH by lia.
@@ -264,7 +264,7 @@ Section mjoin.
     split; [|naive_solver].
     destruct 1 as (j'&l'&i'&?&?&Hj); decompose_Forall.
     assert (i' < length l') by eauto using lookup_lt_Some.
-    apply Nat_mul_split_l in Hj; naive_solver.
+    apply Nat.mul_split_l in Hj; naive_solver.
   Qed.
 End mjoin.
 
@@ -315,16 +315,16 @@ Section Z_little_endian.
     intros -> ?. induction 1 as [|b bs ? ? IH]; [done|]; simpl.
     rewrite Nat2Z.inj_succ, Z_to_little_endian_succ by lia. f_equal.
     - apply Z.bits_inj_iff'. intros z' ?.
-      rewrite !Z.land_spec, Z.lor_spec, Z_ones_spec by lia.
+      rewrite !Z.land_spec, Z.lor_spec, Z.ones_spec by lia.
       case_bool_decide.
       + rewrite andb_true_r, Z.shiftl_spec_low, orb_false_r by lia. done.
       + rewrite andb_false_r.
-        symmetry. eapply (Z_bounded_iff_bits_nonneg n); lia.
+        symmetry. eapply (Z.bounded_iff_bits_nonneg n); lia.
     - rewrite <-IH at 3. f_equal.
       apply Z.bits_inj_iff'. intros z' ?.
       rewrite Z.shiftr_spec, Z.lor_spec, Z.shiftl_spec by lia.
       assert (Z.testbit b (z' + n) = false) as ->.
-      { apply (Z_bounded_iff_bits_nonneg n); lia. }
+      { apply (Z.bounded_iff_bits_nonneg n); lia. }
       rewrite orb_false_l. f_equal. lia.
   Qed.
 
@@ -334,17 +334,17 @@ Section Z_little_endian.
   Proof.
     intros ? Hm. rewrite <-Z.land_ones by lia.
     revert z.
-    induction m as [|m ? IH|] using (Z_succ_pred_induction 0); intros z; [..|lia].
+    induction m as [|m ? IH|] using (Z.succ_pred_induction 0); intros z; [..|lia].
     { Z.bitwise. by rewrite andb_false_r. }
     rewrite Z_to_little_endian_succ by lia; simpl. rewrite IH by lia.
     apply Z.bits_inj_iff'. intros z' ?.
     rewrite Z.land_spec, Z.lor_spec, Z.shiftl_spec, !Z.land_spec by lia.
-    rewrite (Z_ones_spec n z') by lia. case_bool_decide.
+    rewrite (Z.ones_spec n z') by lia. case_bool_decide.
     - rewrite andb_true_r, (Z.testbit_neg_r _ (z' - n)), orb_false_r by lia. simpl.
-      by rewrite Z_ones_spec, bool_decide_true, andb_true_r by lia.
+      by rewrite Z.ones_spec, bool_decide_true, andb_true_r by lia.
     - rewrite andb_false_r, orb_false_l.
       rewrite Z.shiftr_spec by lia. f_equal; [f_equal; lia|].
-      rewrite !Z_ones_spec by lia. apply bool_decide_ext. lia.
+      rewrite !Z.ones_spec by lia. apply bool_decide_ext. lia.
   Qed.
 
   Lemma Z_to_little_endian_length m n z :
@@ -352,7 +352,7 @@ Section Z_little_endian.
     Z.of_nat (length (Z_to_little_endian m n z)) = m.
   Proof.
     intros. revert z. induction m as [|m ? IH|]
-      using (Z_succ_pred_induction 0); intros z; [done| |lia].
+      using (Z.succ_pred_induction 0); intros z; [done| |lia].
     rewrite Z_to_little_endian_succ by lia. simpl. by rewrite Nat2Z.inj_succ, IH.
   Qed.
 
@@ -361,7 +361,7 @@ Section Z_little_endian.
     Forall (λ b, 0 ≤ b < 2 ^ n) (Z_to_little_endian m n z).
   Proof.
     intros. revert z.
-    induction m as [|m ? IH|] using (Z_succ_pred_induction 0); intros z; [..|lia].
+    induction m as [|m ? IH|] using (Z.succ_pred_induction 0); intros z; [..|lia].
     { by constructor. }
     rewrite Z_to_little_endian_succ by lia.
     constructor; [|by apply IH]. rewrite Z.land_ones by lia.
@@ -374,12 +374,12 @@ Section Z_little_endian.
     0 ≤ little_endian_to_Z n bs < 2 ^ (Z.of_nat (length bs) * n).
   Proof.
     intros ?. induction 1 as [|b bs Hb ? IH]; [done|]; simpl.
-    apply Z_bounded_iff_bits_nonneg'; [lia|..].
+    apply Z.bounded_iff_bits_nonneg'; [lia|..].
     { apply Z.lor_nonneg. split; [lia|]. apply Z.shiftl_nonneg. lia. }
     intros z' ?. rewrite Z.lor_spec.
-    rewrite Z_bounded_iff_bits_nonneg' in Hb by lia.
+    rewrite Z.bounded_iff_bits_nonneg' in Hb by lia.
     rewrite Hb, orb_false_l, Z.shiftl_spec by lia.
-    apply (Z_bounded_iff_bits_nonneg' (Z.of_nat (length bs) * n)); lia.
+    apply (Z.bounded_iff_bits_nonneg' (Z.of_nat (length bs) * n)); lia.
   Qed.
 
   Lemma Z_to_little_endian_lookup_Some m n z (i : nat) x :
@@ -387,7 +387,7 @@ Section Z_little_endian.
     Z_to_little_endian m n z !! i = Some x ↔
     Z.of_nat i < m ∧ x = Z.land (z ≫ (Z.of_nat i * n)) (Z.ones n).
   Proof.
-    revert z i. induction m as [|m ? IH|] using (Z_succ_pred_induction 0);
+    revert z i. induction m as [|m ? IH|] using (Z.succ_pred_induction 0);
       intros z i ??; [..|lia].
     { destruct i; simpl; naive_solver lia. }
     rewrite Z_to_little_endian_succ by lia. destruct i as [|i]; simpl.
@@ -415,7 +415,7 @@ Section Z_little_endian.
       rewrite Hdiv in Hlookup; simplify_eq/=.
       rewrite Z.lor_spec, Z.shiftl_spec, IH by auto with lia.
       assert (Z.testbit b' i = false) as ->.
-      { apply (Z_bounded_iff_bits_nonneg n); lia. }
+      { apply (Z.bounded_iff_bits_nonneg n); lia. }
       by rewrite <-Zminus_mod_idemp_r, Z_mod_same_full, Z.sub_0_r.
   Qed.
 End Z_little_endian.
diff --git a/stdpp/nat_cancel.v b/stdpp/nat_cancel.v
index d0372a22a20fe297667b11cbfc008f3ede198dee..1fac15932f41d606c22e77d087d36d67cdd06232 100644
--- a/stdpp/nat_cancel.v
+++ b/stdpp/nat_cancel.v
@@ -64,22 +64,22 @@ Module nat_cancel.
   Global Instance make_nat_S_1 n : MakeNatS 1 n (S n).
   Proof. done. Qed.
 
-  Class MakeNatPlus (n1 n2 m : nat) := make_nat_plus : m = n1 + n2.
-  Global Instance make_nat_plus_0_l n : MakeNatPlus 0 n n.
+  Class MakeNatAdd (n1 n2 m : nat) := make_nat_add : m = n1 + n2.
+  Global Instance make_nat_add_0_l n : MakeNatAdd 0 n n.
   Proof. done. Qed.
-  Global Instance make_nat_plus_0_r n : MakeNatPlus n 0 n.
-  Proof. unfold MakeNatPlus. by rewrite Nat.add_0_r. Qed.
-  Global Instance make_nat_plus_default n1 n2 : MakeNatPlus n1 n2 (n1 + n2) | 100.
+  Global Instance make_nat_add_0_r n : MakeNatAdd n 0 n.
+  Proof. unfold MakeNatAdd. by rewrite Nat.add_0_r. Qed.
+  Global Instance make_nat_add_default n1 n2 : MakeNatAdd n1 n2 (n1 + n2) | 100.
   Proof. done. Qed.
 
   Global Instance nat_cancel_leaf_here m : NatCancelR m m 0 0 | 0.
   Proof. by unfold NatCancelR, NatCancelL. Qed.
   Global Instance nat_cancel_leaf_else m n : NatCancelR m n m n | 100.
   Proof. by unfold NatCancelR. Qed.
-  Global Instance nat_cancel_leaf_plus m m' m'' n1 n2 n1' n2' n1'n2' :
+  Global Instance nat_cancel_leaf_add m m' m'' n1 n2 n1' n2' n1'n2' :
     NatCancelR m n1 m' n1' → NatCancelR m' n2 m'' n2' →
-    MakeNatPlus n1' n2' n1'n2' → NatCancelR m (n1 + n2) m'' n1'n2' | 2.
-  Proof. unfold NatCancelR, NatCancelL, MakeNatPlus. lia. Qed.
+    MakeNatAdd n1' n2' n1'n2' → NatCancelR m (n1 + n2) m'' n1'n2' | 2.
+  Proof. unfold NatCancelR, NatCancelL, MakeNatAdd. lia. Qed.
   Global Instance nat_cancel_leaf_S_here m n m' n' :
     NatCancelR m n m' n' → NatCancelR (S m) (S n) m' n' | 3.
   Proof. unfold NatCancelR, NatCancelL. lia. Qed.
@@ -92,10 +92,10 @@ Module nat_cancel.
   Global Instance nat_cancel_S_both m n m' n' :
     NatCancelL m n m' n' → NatCancelL (S m) (S n) m' n' | 1.
   Proof. unfold NatCancelL. lia. Qed.
-  Global Instance nat_cancel_plus m1 m2 m1' m2' m1'm2' n n' n'' :
+  Global Instance nat_cancel_add m1 m2 m1' m2' m1'm2' n n' n'' :
     NatCancelL m1 n m1' n' → NatCancelL m2 n' m2' n'' →
-    MakeNatPlus m1' m2' m1'm2' → NatCancelL (m1 + m2) n m1'm2' n'' | 2.
-  Proof. unfold NatCancelL, MakeNatPlus. lia. Qed.
+    MakeNatAdd m1' m2' m1'm2' → NatCancelL (m1 + m2) n m1'm2' n'' | 2.
+  Proof. unfold NatCancelL, MakeNatAdd. lia. Qed.
   Global Instance nat_cancel_S m m' m'' Sm' n n' n'' :
     NatCancelL m n m' n' → NatCancelR 1 n' m'' n'' →
     MakeNatS m'' m' Sm' → NatCancelL (S m) n Sm' n'' | 3.
diff --git a/stdpp/numbers.v b/stdpp/numbers.v
index 4f72314302e0bfea69cae39fd9fda484d4e258cc..315066f37deb20ada9b01020b426b5058308e33f 100644
--- a/stdpp/numbers.v
+++ b/stdpp/numbers.v
@@ -1,6 +1,26 @@
-(** This file collects some trivial facts on the Coq types [nat] and [N] for
-natural numbers, and the type [Z] for integers. It also declares some useful
-notations. *)
+(** This file provides various tweaks and extensions to Coq's theory of numbers
+(natural numbers [nat] and [N], positive numbers [positive], integers [Z], and
+rationals [Qc]). In addition, this file defines a new type of positive rational
+numbers [Qp], which is used extensively in Iris to represent fractional
+permissions.
+
+The organization of this file follows mostly Coq's standard library.
+
+- We put all results in modules. For example, the module [Nat] collects the
+  results for type [nat]. Since the Coq stdlib already defines a module [Nat],
+  our module [Nat] exports Coq's module so that our module [Nat] contains the
+  union of the results from the Coq stdlib and std++.
+- We follow the naming convention of Coq's "numbers" library to prefer
+  [succ]/[add]/[sub]/[mul] over [S]/[plus]/[minus]/[mult].
+- One typically does not [Import] modules such as [Nat], and refers to the
+  results using [Nat.lem]. As a consequence, all [Hint]s [Instance]s in the modules in
+  this file are [Global] and not [Export]. Other things like [Arguments] are outside
+  the modules, since for them [Global] works like [Export].
+
+The results for [Qc] are not yet in a module. This is in part because they
+still follow the old/non-module style in Coq's standard library. See also
+https://gitlab.mpi-sws.org/iris/stdpp/-/issues/147. *)
+
 From Coq Require Export EqdepFacts PArith NArith ZArith NPeano.
 From Coq Require Import QArith Qcanon.
 From stdpp Require Export base decidable option.
@@ -11,9 +31,11 @@ Global Instance comparison_eq_dec : EqDecision comparison.
 Proof. solve_decision. Defined.
 
 (** * Notations and properties of [nat] *)
-Global Arguments minus !_ !_ / : assert.
+Global Arguments Nat.sub !_ !_ / : assert.
 Global Arguments Nat.max : simpl nomatch.
 
+(** We do not make [Nat.lt] since it is an alias for [lt], which contains the
+actual definition that we want to make opaque. *)
 Typeclasses Opaque lt.
 
 Reserved Notation "x ≤ y ≤ z" (at level 70, y at next level).
@@ -36,87 +58,96 @@ Infix "`mod`" := Nat.modulo (at level 35) : nat_scope.
 Infix "`max`" := Nat.max (at level 35) : nat_scope.
 Infix "`min`" := Nat.min (at level 35) : nat_scope.
 
-Global Instance nat_eq_dec: EqDecision nat := eq_nat_dec.
-Global Instance nat_le_dec: RelDecision le := le_dec.
-Global Instance nat_lt_dec: RelDecision lt := lt_dec.
-Global Instance nat_inhabited: Inhabited nat := populate 0%nat.
-Global Instance S_inj: Inj (=) (=) S.
-Proof. by injection 1. Qed.
-Global Instance nat_le_po: PartialOrder (≤).
-Proof. repeat split; repeat intro; auto with lia. Qed.
-Global Instance nat_le_total: Total (≤).
-Proof. repeat intro; lia. Qed.
-
-Global Instance nat_le_pi: ∀ x y : nat, ProofIrrel (x ≤ y).
-Proof.
-  assert (∀ x y (p : x ≤ y) y' (q : x ≤ y'),
-    y = y' → eq_dep nat (le x) y p y' q) as aux.
-  { fix FIX 3. intros x ? [|y p] ? [|y' q].
-    - done.
-    - clear FIX. intros; exfalso; auto with lia.
-    - clear FIX. intros; exfalso; auto with lia.
-    - injection 1. intros Hy. by case (FIX x y p y' q Hy). }
-  intros x y p q.
-  by apply (Eqdep_dec.eq_dep_eq_dec (λ x y, decide (x = y))), aux.
-Qed.
-Global Instance nat_lt_pi: ∀ x y : nat, ProofIrrel (x < y).
-Proof. unfold lt. apply _. Qed.
-
-Lemma nat_le_sum (x y : nat) : x ≤ y ↔ ∃ z, y = x + z.
-Proof. split; [exists (y - x); lia | intros [z ->]; lia]. Qed.
-
-(** [Arith.Minus.minus_plus] is deprecated starting in 8.16 *)
-Lemma nat_minus_plus n m : n + m - n = m.
-Proof. lia. Qed.
-(** [Arith.Minus.le_plus_minus] is deprecated starting in 8.16 *)
-Lemma nat_le_plus_minus n m : n ≤ m → m = n + (m - n).
-Proof. lia. Qed.
-
-Lemma Nat_lt_succ_succ n : n < S (S n).
-Proof. auto with arith. Qed.
-Lemma Nat_mul_split_l n x1 x2 y1 y2 :
-  x2 < n → y2 < n → x1 * n + x2 = y1 * n + y2 → x1 = y1 ∧ x2 = y2.
-Proof.
-  intros Hx2 Hy2 E. cut (x1 = y1); [intros; subst;lia |].
-  revert y1 E. induction x1; simpl; intros [|?]; simpl; auto with lia.
-Qed.
-Lemma Nat_mul_split_r n x1 x2 y1 y2 :
-  x1 < n → y1 < n → x1 + x2 * n = y1 + y2 * n → x1 = y1 ∧ x2 = y2.
-Proof. intros. destruct (Nat_mul_split_l n x2 x1 y2 y1); auto with lia. Qed.
-
+(** TODO: Consider removing these notations to avoid populting the global
+scope? *)
 Notation lcm := Nat.lcm.
 Notation divide := Nat.divide.
 Notation "( x | y )" := (divide x y) : nat_scope.
-Global Instance Nat_divide_dec : RelDecision Nat.divide.
-Proof.
-  refine (λ x y, cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff.
-Defined.
-Global Instance: PartialOrder divide.
-Proof.
-  repeat split; try apply _. intros ??. apply Nat.divide_antisym_nonneg; lia.
-Qed.
-Global Hint Extern 0 (_ | _) => reflexivity : core.
-Lemma Nat_divide_ne_0 x y : (x | y) → y ≠ 0 → x ≠ 0.
-Proof. intros Hxy Hy ->. by apply Hy, Nat.divide_0_l. Qed.
-
-Lemma Nat_iter_S {A} n (f: A → A) x : Nat.iter (S n) f x = f (Nat.iter n f x).
-Proof. done. Qed.
-Lemma Nat_iter_S_r {A} n (f: A → A) x : Nat.iter (S n) f x = Nat.iter n f (f x).
-Proof. induction n; by f_equal/=. Qed.
-Lemma Nat_iter_add {A} n1 n2 (f : A → A) x :
-  Nat.iter (n1 + n2) f x = Nat.iter n1 f (Nat.iter n2 f x).
-Proof. induction n1; by f_equal/=. Qed.
-Lemma Nat_iter_mul {A} n1 n2 (f : A → A) x :
-  Nat.iter (n1 * n2) f x = Nat.iter n1 (Nat.iter n2 f) x.
-Proof.
-  intros. induction n1 as [|n1 IHn1]; [done|].
-  simpl. by rewrite Nat_iter_add, IHn1.
-Qed.
-
-Lemma Nat_iter_ind {A} (P : A → Prop) f x k :
-  P x → (∀ y, P y → P (f y)) → P (Nat.iter k f x).
-Proof. induction k; simpl; auto. Qed.
 
+Module Nat.
+  Export PeanoNat.Nat.
+
+  Global Instance eq_dec: EqDecision nat := eq_nat_dec.
+  Global Instance le_dec: RelDecision le := le_dec.
+  Global Instance lt_dec: RelDecision lt := lt_dec.
+  Global Instance inhabited: Inhabited nat := populate 0.
+
+  Global Instance succ_inj: Inj (=) (=) Nat.succ.
+  Proof. by injection 1. Qed.
+
+  Global Instance le_po: PartialOrder (≤).
+  Proof. repeat split; repeat intro; auto with lia. Qed.
+  Global Instance le_total: Total (≤).
+  Proof. repeat intro; lia. Qed.
+
+  Global Instance le_pi: ∀ x y : nat, ProofIrrel (x ≤ y).
+  Proof.
+    assert (∀ x y (p : x ≤ y) y' (q : x ≤ y'),
+      y = y' → eq_dep nat (le x) y p y' q) as aux.
+    { fix FIX 3. intros x ? [|y p] ? [|y' q].
+      - done.
+      - clear FIX. intros; exfalso; auto with lia.
+      - clear FIX. intros; exfalso; auto with lia.
+      - injection 1. intros Hy. by case (FIX x y p y' q Hy). }
+    intros x y p q.
+    by apply (Eqdep_dec.eq_dep_eq_dec (λ x y, decide (x = y))), aux.
+  Qed.
+  Global Instance lt_pi: ∀ x y : nat, ProofIrrel (x < y).
+  Proof. unfold Peano.lt. apply _. Qed.
+
+  Lemma le_sum (x y : nat) : x ≤ y ↔ ∃ z, y = x + z.
+  Proof. split; [exists (y - x); lia | intros [z ->]; lia]. Qed.
+
+  (** [Arith.Minus.minus_plus] is deprecated starting in 8.16 *)
+  Lemma sub_add' n m : n + m - n = m.
+  Proof. lia. Qed.
+  (** [Arith.Minus.le_plus_minus] is deprecated starting in 8.16 *)
+  Lemma le_add_sub n m : n ≤ m → m = n + (m - n).
+  Proof. lia. Qed.
+
+  Lemma lt_succ_succ n : n < S (S n).
+  Proof. auto with arith. Qed.
+  Lemma mul_split_l n x1 x2 y1 y2 :
+    x2 < n → y2 < n → x1 * n + x2 = y1 * n + y2 → x1 = y1 ∧ x2 = y2.
+  Proof.
+    intros Hx2 Hy2 E. cut (x1 = y1); [intros; subst;lia |].
+    revert y1 E. induction x1; simpl; intros [|?]; simpl; auto with lia.
+  Qed.
+  Lemma mul_split_r n x1 x2 y1 y2 :
+    x1 < n → y1 < n → x1 + x2 * n = y1 + y2 * n → x1 = y1 ∧ x2 = y2.
+  Proof. intros. destruct (mul_split_l n x2 x1 y2 y1); auto with lia. Qed.
+
+  Global Instance divide_dec : RelDecision Nat.divide.
+  Proof.
+    refine (λ x y, cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff.
+  Defined.
+  Global Instance divide_po : PartialOrder divide.
+  Proof.
+    repeat split; try apply _. intros ??. apply Nat.divide_antisym_nonneg; lia.
+  Qed.
+  Global Hint Extern 0 (_ | _) => reflexivity : core.
+
+  Lemma divide_ne_0 x y : (x | y) → y ≠ 0 → x ≠ 0.
+  Proof. intros Hxy Hy ->. by apply Hy, Nat.divide_0_l. Qed.
+
+  Lemma iter_succ {A} n (f: A → A) x : Nat.iter (S n) f x = f (Nat.iter n f x).
+  Proof. done. Qed.
+  Lemma iter_succ_r {A} n (f: A → A) x : Nat.iter (S n) f x = Nat.iter n f (f x).
+  Proof. induction n; by f_equal/=. Qed.
+  Lemma iter_add {A} n1 n2 (f : A → A) x :
+    Nat.iter (n1 + n2) f x = Nat.iter n1 f (Nat.iter n2 f x).
+  Proof. induction n1; by f_equal/=. Qed.
+  Lemma iter_mul {A} n1 n2 (f : A → A) x :
+    Nat.iter (n1 * n2) f x = Nat.iter n1 (Nat.iter n2 f) x.
+  Proof.
+    intros. induction n1 as [|n1 IHn1]; [done|].
+    simpl. by rewrite iter_add, IHn1.
+  Qed.
+
+  Lemma iter_ind {A} (P : A → Prop) f x k :
+    P x → (∀ y, P y → P (f y)) → P (Nat.iter k f x).
+  Proof. induction k; simpl; auto. Qed.
+End Nat.
 
 (** * Notations and properties of [positive] *)
 Local Open Scope positive_scope.
@@ -135,154 +166,162 @@ Notation "(~0)" := xO (only parsing) : positive_scope.
 Notation "(~1)" := xI (only parsing) : positive_scope.
 
 Global Arguments Pos.of_nat : simpl never.
-Global Arguments Pmult : simpl never.
-
-Global Instance positive_eq_dec: EqDecision positive := Pos.eq_dec.
-Global Instance positive_le_dec: RelDecision Pos.le.
-Proof. refine (λ x y, decide ((x ?= y) ≠ Gt)). Defined.
-Global Instance positive_lt_dec: RelDecision Pos.lt.
-Proof. refine (λ x y, decide ((x ?= y) = Lt)). Defined.
-Global Instance positive_le_total: Total Pos.le.
-Proof. repeat intro; lia. Qed.
-
-Global Instance positive_inhabited: Inhabited positive := populate 1.
-
-Global Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end.
-Global Instance maybe_xI : Maybe xI := λ p, match p with p~1 => Some p | _ => None end.
-Global Instance xO_inj : Inj (=) (=) (~0).
-Proof. by injection 1. Qed.
-Global Instance xI_inj : Inj (=) (=) (~1).
-Proof. by injection 1. Qed.
-
-(** Since [positive] represents lists of bits, we define list operations
-on it. These operations are in reverse, as positives are treated as snoc
-lists instead of cons lists. *)
-Fixpoint Papp (p1 p2 : positive) : positive :=
-  match p2 with
-  | 1 => p1
-  | p2~0 => (Papp p1 p2)~0
-  | p2~1 => (Papp p1 p2)~1
-  end.
-Infix "++" := Papp : positive_scope.
-Notation "(++)" := Papp (only parsing) : positive_scope.
-Notation "( p ++.)" := (Papp p) (only parsing) : positive_scope.
-Notation "(.++ q )" := (λ p, Papp p q) (only parsing) : positive_scope.
-
-Fixpoint Preverse_go (p1 p2 : positive) : positive :=
-  match p2 with
-  | 1 => p1
-  | p2~0 => Preverse_go (p1~0) p2
-  | p2~1 => Preverse_go (p1~1) p2
-  end.
-Definition Preverse : positive → positive := Preverse_go 1.
-
-Global Instance Papp_1_l : LeftId (=) 1 (++).
-Proof. intros p. by induction p; intros; f_equal/=. Qed.
-Global Instance Papp_1_r : RightId (=) 1 (++).
-Proof. done. Qed.
-Global Instance Papp_assoc : Assoc (=) (++).
-Proof. intros ?? p. by induction p; intros; f_equal/=. Qed.
-Global Instance Papp_inj p : Inj (=) (=) (.++ p).
-Proof. intros ???. induction p; simplify_eq; auto. Qed.
-
-Lemma Preverse_go_app p1 p2 p3 :
-  Preverse_go p1 (p2 ++ p3) = Preverse_go p1 p3 ++ Preverse_go 1 p2.
-Proof.
-  revert p3 p1 p2.
-  cut (∀ p1 p2 p3, Preverse_go (p2 ++ p3) p1 = p2 ++ Preverse_go p3 p1).
-  { by intros go p3; induction p3; intros p1 p2; simpl; auto; rewrite <-?go. }
-  intros p1; induction p1 as [p1 IH|p1 IH|]; intros p2 p3; simpl; auto.
-  - apply (IH _ (_~1)).
-  - apply (IH _ (_~0)).
-Qed.
-Lemma Preverse_app p1 p2 : Preverse (p1 ++ p2) = Preverse p2 ++ Preverse p1.
-Proof. unfold Preverse. by rewrite Preverse_go_app. Qed.
-Lemma Preverse_xO p : Preverse (p~0) = (1~0) ++ Preverse p.
-Proof Preverse_app p (1~0).
-Lemma Preverse_xI p : Preverse (p~1) = (1~1) ++ Preverse p.
-Proof Preverse_app p (1~1).
-
-Lemma Preverse_involutive p :
-  Preverse (Preverse p) = p.
-Proof.
-  induction p as [p IH|p IH|]; simpl.
-  - by rewrite Preverse_xI, Preverse_app, IH.
-  - by rewrite Preverse_xO, Preverse_app, IH.
-  - reflexivity.
-Qed.
-
-Global Instance Preverse_inj : Inj (=) (=) Preverse.
-Proof.
-  intros p q eq.
-  rewrite <- (Preverse_involutive p).
-  rewrite <- (Preverse_involutive q).
-  by rewrite eq.
-Qed.
-
-Fixpoint Plength (p : positive) : nat :=
-  match p with 1 => 0%nat | p~0 | p~1 => S (Plength p) end.
-Lemma Papp_length p1 p2 : Plength (p1 ++ p2) = (Plength p2 + Plength p1)%nat.
-Proof. by induction p2; f_equal/=. Qed.
-
-Lemma Plt_sum (x y : positive) : x < y ↔ ∃ z, y = x + z.
-Proof.
-  split.
-  - exists (y - x)%positive. symmetry. apply Pplus_minus. lia.
-  - intros [z ->]. lia.
-Qed.
-
-(** Duplicate the bits of a positive, i.e. 1~0~1 -> 1~0~0~1~1 and
-    1~1~0~0 -> 1~1~1~0~0~0~0 *)
-Fixpoint Pdup (p : positive) : positive :=
-  match p with
-  | 1 => 1
-  | p'~0 => (Pdup p')~0~0
-  | p'~1 => (Pdup p')~1~1
-  end.
-
-Lemma Pdup_app p q :
-  Pdup (p ++ q) = Pdup p ++ Pdup q.
-Proof.
-  revert p.
-  induction q as [p IH|p IH|]; intros q; simpl.
-  - by rewrite IH.
-  - by rewrite IH.
-  - reflexivity.
-Qed.
-
-Lemma Pdup_suffix_eq p q s1 s2 :
-  s1~1~0 ++ Pdup p = s2~1~0 ++ Pdup q → p = q.
-Proof.
-  revert q.
-  induction p as [p IH|p IH|]; intros [q|q|] eq; simplify_eq/=.
-  - by rewrite (IH q).
-  - by rewrite (IH q).
-  - reflexivity.
-Qed.
-
-Global Instance Pdup_inj : Inj (=) (=) Pdup.
-Proof.
-  intros p q eq.
-  apply (Pdup_suffix_eq _ _ 1 1).
-  by rewrite eq.
-Qed.
-
-Lemma Preverse_Pdup p :
-  Preverse (Pdup p) = Pdup (Preverse p).
-Proof.
-  induction p as [p IH|p IH|]; simpl.
-  - rewrite 3!Preverse_xI.
-    rewrite (assoc_L (++)).
-    rewrite IH.
-    rewrite Pdup_app.
-    reflexivity.
-  - rewrite 3!Preverse_xO.
-    rewrite (assoc_L (++)).
-    rewrite IH.
-    rewrite Pdup_app.
-    reflexivity.
-  - reflexivity.
-Qed.
+Global Arguments Pos.mul : simpl never.
+
+Module Pos.
+  Export BinPos.Pos.
+
+  Global Instance eq_dec: EqDecision positive := Pos.eq_dec.
+  Global Instance le_dec: RelDecision Pos.le.
+  Proof. refine (λ x y, decide ((x ?= y) ≠ Gt)). Defined.
+  Global Instance lt_dec: RelDecision Pos.lt.
+  Proof. refine (λ x y, decide ((x ?= y) = Lt)). Defined.
+  Global Instance le_total: Total Pos.le.
+  Proof. repeat intro; lia. Qed.
+
+  Global Instance inhabited: Inhabited positive := populate 1.
+
+  Global Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end.
+  Global Instance maybe_xI : Maybe xI := λ p, match p with p~1 => Some p | _ => None end.
+  Global Instance xO_inj : Inj (=) (=) (~0).
+  Proof. by injection 1. Qed.
+  Global Instance xI_inj : Inj (=) (=) (~1).
+  Proof. by injection 1. Qed.
+
+  (** Since [positive] represents lists of bits, we define list operations
+  on it. These operations are in reverse, as positives are treated as snoc
+  lists instead of cons lists. *)
+  Fixpoint app (p1 p2 : positive) : positive :=
+    match p2 with
+    | 1 => p1
+    | p2~0 => (app p1 p2)~0
+    | p2~1 => (app p1 p2)~1
+    end.
+
+  Module Import app_notations.
+    Infix "++" := app : positive_scope.
+    Notation "(++)" := app (only parsing) : positive_scope.
+    Notation "( p ++.)" := (app p) (only parsing) : positive_scope.
+    Notation "(.++ q )" := (λ p, app p q) (only parsing) : positive_scope.
+  End app_notations.
+
+  Fixpoint reverse_go (p1 p2 : positive) : positive :=
+    match p2 with
+    | 1 => p1
+    | p2~0 => reverse_go (p1~0) p2
+    | p2~1 => reverse_go (p1~1) p2
+    end.
+  Definition reverse : positive → positive := reverse_go 1.
+
+  Global Instance app_1_l : LeftId (=) 1 (++).
+  Proof. intros p. by induction p; intros; f_equal/=. Qed.
+  Global Instance app_1_r : RightId (=) 1 (++).
+  Proof. done. Qed.
+  Global Instance app_assoc : Assoc (=) (++).
+  Proof. intros ?? p. by induction p; intros; f_equal/=. Qed.
+  Global Instance app_inj p : Inj (=) (=) (.++ p).
+  Proof. intros ???. induction p; simplify_eq; auto. Qed.
+
+  Lemma reverse_go_app p1 p2 p3 :
+    reverse_go p1 (p2 ++ p3) = reverse_go p1 p3 ++ reverse_go 1 p2.
+  Proof.
+    revert p3 p1 p2.
+    cut (∀ p1 p2 p3, reverse_go (p2 ++ p3) p1 = p2 ++ reverse_go p3 p1).
+    { by intros go p3; induction p3; intros p1 p2; simpl; auto; rewrite <-?go. }
+    intros p1; induction p1 as [p1 IH|p1 IH|]; intros p2 p3; simpl; auto.
+    - apply (IH _ (_~1)).
+    - apply (IH _ (_~0)).
+  Qed.
+  Lemma reverse_app p1 p2 : reverse (p1 ++ p2) = reverse p2 ++ reverse p1.
+  Proof. unfold reverse. by rewrite reverse_go_app. Qed.
+  Lemma reverse_xO p : reverse (p~0) = (1~0) ++ reverse p.
+  Proof reverse_app p (1~0).
+  Lemma reverse_xI p : reverse (p~1) = (1~1) ++ reverse p.
+  Proof reverse_app p (1~1).
+
+  Lemma reverse_involutive p : reverse (reverse p) = p.
+  Proof.
+    induction p as [p IH|p IH|]; simpl.
+    - by rewrite reverse_xI, reverse_app, IH.
+    - by rewrite reverse_xO, reverse_app, IH.
+    - reflexivity.
+  Qed.
+
+  Global Instance reverse_inj : Inj (=) (=) reverse.
+  Proof.
+    intros p q eq.
+    rewrite <-(reverse_involutive p).
+    rewrite <-(reverse_involutive q).
+    by rewrite eq.
+  Qed.
+
+  Fixpoint length (p : positive) : nat :=
+    match p with 1 => 0%nat | p~0 | p~1 => S (length p) end.
+  Lemma app_length p1 p2 : length (p1 ++ p2) = (length p2 + length p1)%nat.
+  Proof. by induction p2; f_equal/=. Qed.
+
+  Lemma lt_sum (x y : positive) : x < y ↔ ∃ z, y = x + z.
+  Proof.
+    split.
+    - exists (y - x)%positive. symmetry. apply Pplus_minus. lia.
+    - intros [z ->]. lia.
+  Qed.
+
+  (** Duplicate the bits of a positive, i.e. 1~0~1 -> 1~0~0~1~1 and
+      1~1~0~0 -> 1~1~1~0~0~0~0 *)
+  Fixpoint dup (p : positive) : positive :=
+    match p with
+    | 1 => 1
+    | p'~0 => (dup p')~0~0
+    | p'~1 => (dup p')~1~1
+    end.
+
+  Lemma dup_app p q :
+    dup (p ++ q) = dup p ++ dup q.
+  Proof.
+    revert p.
+    induction q as [p IH|p IH|]; intros q; simpl.
+    - by rewrite IH.
+    - by rewrite IH.
+    - reflexivity.
+  Qed.
+
+  Lemma dup_suffix_eq p q s1 s2 :
+    s1~1~0 ++ dup p = s2~1~0 ++ dup q → p = q.
+  Proof.
+    revert q.
+    induction p as [p IH|p IH|]; intros [q|q|] eq; simplify_eq/=.
+    - by rewrite (IH q).
+    - by rewrite (IH q).
+    - reflexivity.
+  Qed.
+
+  Global Instance dup_inj : Inj (=) (=) dup.
+  Proof.
+    intros p q eq.
+    apply (dup_suffix_eq _ _ 1 1).
+    by rewrite eq.
+  Qed.
+
+  Lemma reverse_dup p :
+    reverse (dup p) = dup (reverse p).
+  Proof.
+    induction p as [p IH|p IH|]; simpl.
+    - rewrite 3!reverse_xI.
+      rewrite (assoc_L (++)).
+      rewrite IH.
+      rewrite dup_app.
+      reflexivity.
+    - rewrite 3!reverse_xO.
+      rewrite (assoc_L (++)).
+      rewrite IH.
+      rewrite dup_app.
+      reflexivity.
+    - reflexivity.
+  Qed.
+End Pos.
+
+Export Pos.app_notations.
 
 Local Close Scope positive_scope.
 
@@ -352,43 +391,6 @@ Infix "≫" := Z.shiftr (at level 35) : Z_scope.
 Infix "`max`" := Z.max (at level 35) : Z_scope.
 Infix "`min`" := Z.min (at level 35) : Z_scope.
 
-Global Instance Zpos_inj : Inj (=) (=) Zpos.
-Proof. by injection 1. Qed.
-Global Instance Zneg_inj : Inj (=) (=) Zneg.
-Proof. by injection 1. Qed.
-
-Global Instance Z_of_nat_inj : Inj (=) (=) Z.of_nat.
-Proof. intros n1 n2. apply Nat2Z.inj. Qed.
-
-Global Instance Z_eq_dec: EqDecision Z := Z.eq_dec.
-Global Instance Z_le_dec: RelDecision Z.le := Z_le_dec.
-Global Instance Z_lt_dec: RelDecision Z.lt := Z_lt_dec.
-Global Instance Z_ge_dec: RelDecision Z.ge := Z_ge_dec.
-Global Instance Z_gt_dec: RelDecision Z.gt := Z_gt_dec.
-Global Instance Z_inhabited: Inhabited Z := populate 1.
-Global Instance Z_lt_pi x y : ProofIrrel (x < y).
-Proof. unfold Z.lt. apply _. Qed.
-
-Global Instance Z_le_po : PartialOrder (≤).
-Proof.
-  repeat split; red; [apply Z.le_refl | apply Z.le_trans | apply Z.le_antisymm].
-Qed.
-Global Instance Z_le_total: Total Z.le.
-Proof. repeat intro; lia. Qed.
-
-Lemma Z_pow_pred_r n m : 0 < m → n * n ^ (Z.pred m) = n ^ m.
-Proof.
-  intros. rewrite <-Z.pow_succ_r, Z.succ_pred; [done|]. by apply Z.lt_le_pred.
-Qed.
-Lemma Z_quot_range_nonneg k x y : 0 ≤ x < k → 0 < y → 0 ≤ x `quot` y < k.
-Proof.
-  intros [??] ?.
-  destruct (decide (y = 1)); subst; [rewrite Z.quot_1_r; auto |].
-  destruct (decide (x = 0)); subst; [rewrite Z.quot_0_l; auto with lia |].
-  split; [apply Z.quot_pos; lia|].
-  trans x; auto. apply Z.quot_lt; lia.
-Qed.
-
 Global Arguments Z.pred : simpl never.
 Global Arguments Z.succ : simpl never.
 Global Arguments Z.of_nat : simpl never.
@@ -415,140 +417,191 @@ Global Arguments Z.lnot : simpl never.
 Global Arguments Z.square : simpl never.
 Global Arguments Z.abs : simpl never.
 
-Lemma Z_to_nat_neq_0_pos x : Z.to_nat x ≠ 0%nat → 0 < x.
-Proof. by destruct x. Qed.
-Lemma Z_to_nat_neq_0_nonneg x : Z.to_nat x ≠ 0%nat → 0 ≤ x.
-Proof. by destruct x. Qed.
-Lemma Z_mod_pos x y : 0 < y → 0 ≤ x `mod` y.
-Proof. apply Z.mod_pos_bound. Qed.
-
-Global Hint Resolve Z.lt_le_incl : zpos.
-Global Hint Resolve Z.add_nonneg_pos Z.add_pos_nonneg Z.add_nonneg_nonneg : zpos.
-Global Hint Resolve Z.mul_nonneg_nonneg Z.mul_pos_pos : zpos.
-Global Hint Resolve Z.pow_pos_nonneg Z.pow_nonneg: zpos.
-Global Hint Resolve Z_mod_pos Z.div_pos : zpos.
-Global Hint Extern 1000 => lia : zpos.
-
-Lemma Z_to_nat_nonpos x : x ≤ 0 → Z.to_nat x = 0%nat.
-Proof. destruct x; simpl; auto using Z2Nat.inj_neg. by intros []. Qed.
-Lemma Z2Nat_inj_pow (x y : nat) : Z.of_nat (x ^ y) = (Z.of_nat x) ^ (Z.of_nat y).
-Proof.
-  induction y as [|y IH]; [by rewrite Z.pow_0_r, Nat.pow_0_r|].
-  by rewrite Nat.pow_succ_r, Nat2Z.inj_succ, Z.pow_succ_r,
-    Nat2Z.inj_mul, IH by auto with zpos.
-Qed.
-Lemma Nat2Z_divide n m : (Z.of_nat n | Z.of_nat m) ↔ (n | m)%nat.
-Proof.
-  split.
-  - rewrite <-(Nat2Z.id m) at 2; intros [i ->]; exists (Z.to_nat i).
-    destruct (decide (0 ≤ i)%Z).
-    { by rewrite Z2Nat.inj_mul, Nat2Z.id by lia. }
-    by rewrite !Z_to_nat_nonpos by auto using Z.mul_nonpos_nonneg with lia.
-  - intros [i ->]. exists (Z.of_nat i). by rewrite Nat2Z.inj_mul.
-Qed.
-Lemma Z2Nat_divide n m :
-  0 ≤ n → 0 ≤ m → (Z.to_nat n | Z.to_nat m)%nat ↔ (n | m).
-Proof. intros. by rewrite <-Nat2Z_divide, !Z2Nat.id by done. Qed.
-Lemma Nat2Z_inj_div x y : Z.of_nat (x `div` y) = (Z.of_nat x) `div` (Z.of_nat y).
-Proof.
-  destruct (decide (y = 0%nat)); [by subst; destruct x |].
-  apply Z.div_unique with (Z.of_nat $ x `mod` y)%nat.
-  { left. rewrite <-(Nat2Z.inj_le 0), <-Nat2Z.inj_lt.
-    apply Nat.mod_bound_pos; lia. }
-  by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod.
-Qed.
-Lemma Nat2Z_inj_mod x y : Z.of_nat (x `mod` y) = (Z.of_nat x) `mod` (Z.of_nat y).
-Proof.
-  destruct (decide (y = 0%nat)); [by subst; destruct x |].
-  apply Z.mod_unique with (Z.of_nat $ x `div` y)%nat.
-  { left. rewrite <-(Nat2Z.inj_le 0), <-Nat2Z.inj_lt.
-    apply Nat.mod_bound_pos; lia. }
-  by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod.
-Qed.
-Lemma Z2Nat_inj_div x y :
-  0 ≤ x → 0 ≤ y →
-  Z.to_nat (x `div` y) = (Z.to_nat x `div` Z.to_nat y)%nat.
-Proof.
-  intros. destruct (decide (y = Z.of_nat 0%nat)); [by subst; destruct x|].
-  pose proof (Z.div_pos x y).
-  apply (inj Z.of_nat). by rewrite Nat2Z_inj_div, !Z2Nat.id by lia.
-Qed.
-Lemma Z2Nat_inj_mod x y :
-  0 ≤ x → 0 ≤ y →
-  Z.to_nat (x `mod` y) = (Z.to_nat x `mod` Z.to_nat y)%nat.
-Proof.
-  intros. destruct (decide (y = Z.of_nat 0%nat)); [by subst; destruct x|].
-  pose proof (Z_mod_pos x y).
-  apply (inj Z.of_nat). by rewrite Nat2Z_inj_mod, !Z2Nat.id by lia.
-Qed.
-Lemma Z_succ_pred_induction y (P : Z → Prop) :
-  P y →
-  (∀ x, y ≤ x → P x → P (Z.succ x)) →
-  (∀ 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.
-
-Lemma Z_ones_spec n m:
-  0 ≤ m → 0 ≤ n →
-  Z.testbit (Z.ones n) m = bool_decide (m < n).
-Proof.
-  intros. case_bool_decide.
-  - by rewrite Z.ones_spec_low by lia.
-  - by rewrite Z.ones_spec_high by lia.
-Qed.
-
-Lemma Z_bounded_iff_bits_nonneg k n :
-  0 ≤ k → 0 ≤ n →
-  n < 2^k ↔ ∀ l, k ≤ l → Z.testbit n l = false.
-Proof.
-  intros. destruct (decide (n = 0)) as [->|].
-  { naive_solver eauto using Z.bits_0, Z.pow_pos_nonneg with lia. }
-  split.
-  { intros Hb%Z.log2_lt_pow2 l Hl; [|lia]. apply Z.bits_above_log2; lia. }
-  intros Hl. apply Z.nle_gt; intros ?.
-  assert (Z.testbit n (Z.log2 n) = false) as Hbit.
-  { apply Hl, Z.log2_le_pow2; lia. }
-  by rewrite Z.bit_log2 in Hbit by lia.
-Qed.
-
-(* Goals of the form [0 ≤ n ≤ 2^k] appear often. So we also define the
-derived version [Z_bounded_iff_bits_nonneg'] that does not require
-proving [0 ≤ n] twice in that case. *)
-Lemma Z_bounded_iff_bits_nonneg' k n :
-  0 ≤ k → 0 ≤ n →
-  0 ≤ n < 2^k ↔ ∀ l, k ≤ l → Z.testbit n l = false.
-Proof. intros ??. rewrite <-Z_bounded_iff_bits_nonneg; lia. Qed.
-
-Lemma Z_bounded_iff_bits k n :
-  0 ≤ k →
-  -2^k ≤ n < 2^k ↔ ∀ l, k ≤ l → Z.testbit n l = bool_decide (n < 0).
-Proof.
-  intros Hk.
-  case_bool_decide; [ | rewrite <-Z_bounded_iff_bits_nonneg; lia].
-  assert(n = - Z.abs n)%Z as -> by lia.
-  split.
-  { intros [? _] l Hl.
-    rewrite Z.bits_opp, negb_true_iff by lia.
-    apply Z_bounded_iff_bits_nonneg with k; lia. }
-  intros Hbit. split.
-  - rewrite <-Z.opp_le_mono, <-Z.lt_pred_le.
-    apply Z_bounded_iff_bits_nonneg; [lia..|]. intros l Hl.
-    rewrite <-negb_true_iff, <-Z.bits_opp by lia.
-    by apply Hbit.
-  - etrans; [|apply Z.pow_pos_nonneg]; lia.
-Qed.
-
-Lemma Z_add_nocarry_lor a b :
-  Z.land a b = 0 →
-  a + b = Z.lor a b.
-Proof. intros ?. rewrite <-Z.lxor_lor by done. by rewrite Z.add_nocarry_lxor. Qed.
-
-Lemma Z_opp_lnot a : -a - 1 = Z.lnot a.
-Proof. pose proof (Z.add_lnot_diag a). lia. Qed.
+Module Z.
+  Export BinInt.Z.
+
+  Global Instance pos_inj : Inj (=) (=) Z.pos.
+  Proof. by injection 1. Qed.
+  Global Instance neg_inj : Inj (=) (=) Z.neg.
+  Proof. by injection 1. Qed.
+
+  Global Instance eq_dec: EqDecision Z := Z.eq_dec.
+  Global Instance le_dec: RelDecision Z.le := Z_le_dec.
+  Global Instance lt_dec: RelDecision Z.lt := Z_lt_dec.
+  Global Instance ge_dec: RelDecision Z.ge := Z_ge_dec.
+  Global Instance gt_dec: RelDecision Z.gt := Z_gt_dec.
+  Global Instance inhabited: Inhabited Z := populate 1.
+  Global Instance lt_pi x y : ProofIrrel (x < y).
+  Proof. unfold Z.lt. apply _. Qed.
+
+  Global Instance le_po : PartialOrder (≤).
+  Proof.
+    repeat split; red; [apply Z.le_refl | apply Z.le_trans | apply Z.le_antisymm].
+  Qed.
+  Global Instance le_total: Total Z.le.
+  Proof. repeat intro; lia. Qed.
+
+  Lemma pow_pred_r n m : 0 < m → n * n ^ (Z.pred m) = n ^ m.
+  Proof.
+    intros. rewrite <-Z.pow_succ_r, Z.succ_pred; [done|]. by apply Z.lt_le_pred.
+  Qed.
+  Lemma quot_range_nonneg k x y : 0 ≤ x < k → 0 < y → 0 ≤ x `quot` y < k.
+  Proof.
+    intros [??] ?.
+    destruct (decide (y = 1)); subst; [rewrite Z.quot_1_r; auto |].
+    destruct (decide (x = 0)); subst; [rewrite Z.quot_0_l; auto with lia |].
+    split; [apply Z.quot_pos; lia|].
+    trans x; auto. apply Z.quot_lt; lia.
+  Qed.
+
+  Lemma mod_pos x y : 0 < y → 0 ≤ x `mod` y.
+  Proof. apply Z.mod_pos_bound. Qed.
+
+  Global Hint Resolve Z.lt_le_incl : zpos.
+  Global Hint Resolve Z.add_nonneg_pos Z.add_pos_nonneg Z.add_nonneg_nonneg : zpos.
+  Global Hint Resolve Z.mul_nonneg_nonneg Z.mul_pos_pos : zpos.
+  Global Hint Resolve Z.pow_pos_nonneg Z.pow_nonneg: zpos.
+  Global Hint Resolve Z.mod_pos Z.div_pos : zpos.
+  Global Hint Extern 1000 => lia : zpos.
+
+  Lemma succ_pred_induction y (P : Z → Prop) :
+    P y →
+    (∀ x, y ≤ x → P x → P (Z.succ x)) →
+    (∀ 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 mod_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.
+
+  Lemma ones_spec n m:
+    0 ≤ m → 0 ≤ n →
+    Z.testbit (Z.ones n) m = bool_decide (m < n).
+  Proof.
+    intros. case_bool_decide.
+    - by rewrite Z.ones_spec_low by lia.
+    - by rewrite Z.ones_spec_high by lia.
+  Qed.
+
+  Lemma bounded_iff_bits_nonneg k n :
+    0 ≤ k → 0 ≤ n →
+    n < 2^k ↔ ∀ l, k ≤ l → Z.testbit n l = false.
+  Proof.
+    intros. destruct (decide (n = 0)) as [->|].
+    { naive_solver eauto using Z.bits_0, Z.pow_pos_nonneg with lia. }
+    split.
+    { intros Hb%Z.log2_lt_pow2 l Hl; [|lia]. apply Z.bits_above_log2; lia. }
+    intros Hl. apply Z.nle_gt; intros ?.
+    assert (Z.testbit n (Z.log2 n) = false) as Hbit.
+    { apply Hl, Z.log2_le_pow2; lia. }
+    by rewrite Z.bit_log2 in Hbit by lia.
+  Qed.
+
+  (* Goals of the form [0 ≤ n ≤ 2^k] appear often. So we also define the
+  derived version [Z_bounded_iff_bits_nonneg'] that does not require
+  proving [0 ≤ n] twice in that case. *)
+  Lemma bounded_iff_bits_nonneg' k n :
+    0 ≤ k → 0 ≤ n →
+    0 ≤ n < 2^k ↔ ∀ l, k ≤ l → Z.testbit n l = false.
+  Proof. intros ??. rewrite <-bounded_iff_bits_nonneg; lia. Qed.
+
+  Lemma bounded_iff_bits k n :
+    0 ≤ k →
+    -2^k ≤ n < 2^k ↔ ∀ l, k ≤ l → Z.testbit n l = bool_decide (n < 0).
+  Proof.
+    intros Hk.
+    case_bool_decide; [ | rewrite <-bounded_iff_bits_nonneg; lia].
+    assert(n = - Z.abs n)%Z as -> by lia.
+    split.
+    { intros [? _] l Hl.
+      rewrite Z.bits_opp, negb_true_iff by lia.
+      apply bounded_iff_bits_nonneg with k; lia. }
+    intros Hbit. split.
+    - rewrite <-Z.opp_le_mono, <-Z.lt_pred_le.
+      apply bounded_iff_bits_nonneg; [lia..|]. intros l Hl.
+      rewrite <-negb_true_iff, <-Z.bits_opp by lia.
+      by apply Hbit.
+    - etrans; [|apply Z.pow_pos_nonneg]; lia.
+  Qed.
+
+  Lemma add_nocarry_lor a b :
+    Z.land a b = 0 →
+    a + b = Z.lor a b.
+  Proof. intros ?. rewrite <-Z.lxor_lor by done. by rewrite Z.add_nocarry_lxor. Qed.
+
+  Lemma opp_lnot a : -a - 1 = Z.lnot a.
+  Proof. pose proof (Z.add_lnot_diag a). lia. Qed.
+End Z.
+
+Module Nat2Z.
+  Export Znat.Nat2Z.
+
+  Global Instance inj' : Inj (=) (=) Z.of_nat.
+  Proof. intros n1 n2. apply Nat2Z.inj. Qed.
+
+  Lemma divide n m : (Z.of_nat n | Z.of_nat m) ↔ (n | m)%nat.
+  Proof.
+    split.
+    - rewrite <-(Nat2Z.id m) at 2; intros [i ->]; exists (Z.to_nat i). lia.
+    - intros [i ->]. exists (Z.of_nat i). by rewrite Nat2Z.inj_mul.
+  Qed.
+  Lemma inj_div x y : Z.of_nat (x `div` y) = (Z.of_nat x) `div` (Z.of_nat y).
+  Proof.
+    destruct (decide (y = 0%nat)); [by subst; destruct x |].
+    apply Z.div_unique with (Z.of_nat $ x `mod` y)%nat.
+    { left. rewrite <-(Nat2Z.inj_le 0), <-Nat2Z.inj_lt.
+      apply Nat.mod_bound_pos; lia. }
+    by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod.
+  Qed.
+  Lemma inj_mod x y : Z.of_nat (x `mod` y) = (Z.of_nat x) `mod` (Z.of_nat y).
+  Proof.
+    destruct (decide (y = 0%nat)); [by subst; destruct x |].
+    apply Z.mod_unique with (Z.of_nat $ x `div` y)%nat.
+    { left. rewrite <-(Nat2Z.inj_le 0), <-Nat2Z.inj_lt.
+      apply Nat.mod_bound_pos; lia. }
+    by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod.
+  Qed.
+End Nat2Z.
+
+Module Z2Nat.
+  Export Znat.Z2Nat.
+
+  Lemma neq_0_pos x : Z.to_nat x ≠ 0%nat → 0 < x.
+  Proof. by destruct x. Qed.
+  Lemma neq_0_nonneg x : Z.to_nat x ≠ 0%nat → 0 ≤ x.
+  Proof. by destruct x. Qed.
+  Lemma nonpos x : x ≤ 0 → Z.to_nat x = 0%nat.
+  Proof. destruct x; simpl; auto using Z2Nat.inj_neg. by intros []. Qed.
+
+  Lemma inj_pow (x y : nat) : Z.of_nat (x ^ y) = (Z.of_nat x) ^ (Z.of_nat y).
+  Proof.
+    induction y as [|y IH]; [by rewrite Z.pow_0_r, Nat.pow_0_r|].
+    by rewrite Nat.pow_succ_r, Nat2Z.inj_succ, Z.pow_succ_r,
+      Nat2Z.inj_mul, IH by auto with zpos.
+  Qed.
+
+  Lemma divide n m :
+    0 ≤ n → 0 ≤ m → (Z.to_nat n | Z.to_nat m)%nat ↔ (n | m).
+  Proof. intros. by rewrite <-Nat2Z.divide, !Z2Nat.id by done. Qed.
+
+  Lemma inj_div x y :
+    0 ≤ x → 0 ≤ y →
+    Z.to_nat (x `div` y) = (Z.to_nat x `div` Z.to_nat y)%nat.
+  Proof.
+    intros. destruct (decide (y = Z.of_nat 0%nat)); [by subst; destruct x|].
+    pose proof (Z.div_pos x y).
+    apply (base.inj Z.of_nat). by rewrite Nat2Z.inj_div, !Z2Nat.id by lia.
+  Qed.
+  Lemma inj_mod x y :
+    0 ≤ x → 0 ≤ y →
+    Z.to_nat (x `mod` y) = (Z.to_nat x `mod` Z.to_nat y)%nat.
+  Proof.
+    intros. destruct (decide (y = Z.of_nat 0%nat)); [by subst; destruct x|].
+    pose proof (Z.mod_pos x y).
+    apply (base.inj Z.of_nat). by rewrite Nat2Z.inj_mod, !Z2Nat.id by lia.
+  Qed.
+End Z2Nat.
 
 (** ** [bool_to_Z] *)
 Definition bool_to_Z (b : bool) : Z :=
@@ -563,15 +616,35 @@ Proof. destruct b; naive_solver. Qed.
 Lemma bool_to_Z_spec b n : Z.testbit (bool_to_Z b) n = bool_decide (n = 0) && b.
 Proof. by destruct b, n. Qed.
 
-
 Local Close Scope Z_scope.
 
+
 (** * Injectivity of casts *)
-Global Instance N_of_nat_inj: Inj (=) (=) N.of_nat := Nat2N.inj.
-Global Instance nat_of_N_inj: Inj (=) (=) N.to_nat := N2Nat.inj.
-Global Instance nat_of_pos_inj: Inj (=) (=) Pos.to_nat := Pos2Nat.inj.
-Global Instance pos_of_Snat_inj: Inj (=) (=) Pos.of_succ_nat := SuccNat2Pos.inj.
-Global Instance Z_of_N_inj: Inj (=) (=) Z.of_N := N2Z.inj.
+Module Nat2N.
+  Export Nnat.Nat2N.
+  Global Instance inj' : Inj (=) (=) N.of_nat := Nat2N.inj.
+End Nat2N.
+
+Module N2Nat.
+  Export Nnat.N2Nat.
+  Global Instance inj' : Inj (=) (=) N.to_nat := N2Nat.inj.
+End N2Nat.
+
+Module Pos2Nat.
+  Export Pnat.Pos2Nat.
+  Global Instance inj' : Inj (=) (=) Pos.to_nat := Pos2Nat.inj.
+End Pos2Nat.
+
+Module SuccNat2Pos.
+  Export Pnat.SuccNat2Pos.
+  Global Instance inj' : Inj (=) (=) Pos.of_succ_nat := SuccNat2Pos.inj.
+End SuccNat2Pos.
+
+Module N2Z.
+  Export Znat.N2Z.
+  Global Instance inj' : Inj (=) (=) Z.of_N := N2Z.inj.
+End N2Z.
+
 (* Add others here. *)
 
 (** * Notations and properties of [Qc] *)
@@ -757,507 +830,514 @@ Add Printing Constructor Qp.
 Bind Scope Qp_scope with Qp.
 Global Arguments Qp_to_Qc _%Qp : assert.
 
-Local Open Scope Qp_scope.
-
-Lemma Qp_to_Qc_inj_iff p q : Qp_to_Qc p = Qp_to_Qc q ↔ p = q.
-Proof.
-  split; [|by intros ->].
-  destruct p, q; intros; simplify_eq/=; f_equal; apply (proof_irrel _).
-Qed.
-Global Instance Qp_eq_dec : EqDecision Qp.
-Proof.
-  refine (λ p q, cast_if (decide (Qp_to_Qc p = Qp_to_Qc q)));
-    by rewrite <-Qp_to_Qc_inj_iff.
-Defined.
-
-Definition Qp_add (p q : Qp) : Qp :=
-  let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
-  mk_Qp (p + q) (Qcplus_pos_pos _ _ Hp Hq).
-Global Arguments Qp_add : simpl never.
-
-Definition Qp_sub (p q : Qp) : option Qp :=
-  let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
-  let pq := (p - q)%Qc in
-  guard (0 < pq)%Qc as Hpq; Some (mk_Qp pq Hpq).
-Global Arguments Qp_sub : simpl never.
-
-Definition Qp_mul (p q : Qp) : Qp :=
-  let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
-  mk_Qp (p * q) (Qcmult_pos_pos _ _ Hp Hq).
-Global Arguments Qp_mul : simpl never.
-
-Definition Qp_inv (q : Qp) : Qp :=
-  let 'mk_Qp q Hq := q return _ in
-  mk_Qp (/ q)%Qc (Qcinv_pos _ Hq).
-Global Arguments Qp_inv : simpl never.
-
-Definition Qp_div (p q : Qp) : Qp := Qp_mul p (Qp_inv q).
-Typeclasses Opaque Qp_div.
-Global Arguments Qp_div : simpl never.
-
-Infix "+" := Qp_add : Qp_scope.
-Infix "-" := Qp_sub : Qp_scope.
-Infix "*" := Qp_mul : Qp_scope.
-Notation "/ q" := (Qp_inv q) : Qp_scope.
-Infix "/" := Qp_div : Qp_scope.
-
-Lemma Qp_to_Qc_inj_add p q : (Qp_to_Qc (p + q) = Qp_to_Qc p + Qp_to_Qc q)%Qc.
-Proof. by destruct p, q. Qed.
-Lemma Qp_to_Qc_inj_mul p q : (Qp_to_Qc (p * q) = Qp_to_Qc p * Qp_to_Qc q)%Qc.
-Proof. by destruct p, q. Qed.
-
 Program Definition pos_to_Qp (n : positive) : Qp := mk_Qp (Qc_of_Z $ Z.pos n) _.
 Next Obligation. intros n. by rewrite <-Z2Qc_inj_0, <-Z2Qc_inj_lt. Qed.
 Global Arguments pos_to_Qp : simpl never.
 
-Notation "1" := (pos_to_Qp 1) : Qp_scope.
-Notation "2" := (pos_to_Qp 2) : Qp_scope.
-Notation "3" := (pos_to_Qp 3) : Qp_scope.
-Notation "4" := (pos_to_Qp 4) : Qp_scope.
-
-Definition Qp_le (p q : Qp) : Prop :=
-  let 'mk_Qp p _ := p in let 'mk_Qp q _ := q in (p ≤ q)%Qc.
-Definition Qp_lt (p q : Qp) : Prop :=
-  let 'mk_Qp p _ := p in let 'mk_Qp q _ := q in (p < q)%Qc.
-
-Infix "≤" := Qp_le : Qp_scope.
-Infix "<" := Qp_lt : Qp_scope.
-Notation "p ≤ q ≤ r" := (p ≤ q ∧ q ≤ r) : Qp_scope.
-Notation "p ≤ q < r" := (p ≤ q ∧ q < r) : Qp_scope.
-Notation "p < q < r" := (p < q ∧ q < r) : Qp_scope.
-Notation "p < q ≤ r" := (p < q ∧ q ≤ r) : Qp_scope.
-Notation "p ≤ q ≤ r ≤ r'" := (p ≤ q ∧ q ≤ r ∧ r ≤ r') : Qp_scope.
-Notation "(≤)" := Qp_le (only parsing) : Qp_scope.
-Notation "(<)" := Qp_lt (only parsing) : Qp_scope.
-
-Global Hint Extern 0 (_ ≤ _)%Qp => reflexivity : core.
-
-Lemma Qp_to_Qc_inj_le p q : p ≤ q ↔ (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc.
-Proof. by destruct p, q. Qed.
-Lemma Qp_to_Qc_inj_lt p q : p < q ↔ (Qp_to_Qc p < Qp_to_Qc q)%Qc.
-Proof. by destruct p, q. Qed.
-
-Global Instance Qp_le_dec : RelDecision (≤).
-Proof.
-  refine (λ p q, cast_if (decide (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc));
-    by rewrite Qp_to_Qc_inj_le.
-Qed.
-Global Instance Qp_lt_dec : RelDecision (<).
-Proof.
-  refine (λ p q, cast_if (decide (Qp_to_Qc p < Qp_to_Qc q)%Qc));
-    by rewrite Qp_to_Qc_inj_lt.
-Qed.
-Global Instance Qp_lt_pi p q : ProofIrrel (p < q).
-Proof. destruct p, q; apply _. Qed.
-
-Definition Qp_max (q p : Qp) : Qp := if decide (q ≤ p) then p else q.
-Definition Qp_min (q p : Qp) : Qp := if decide (q ≤ p) then q else p.
-
-Infix "`max`" := Qp_max : Qp_scope.
-Infix "`min`" := Qp_min : Qp_scope.
-
-Global Instance Qp_inhabited : Inhabited Qp := populate 1.
-
-Global Instance Qp_add_assoc : Assoc (=) Qp_add.
-Proof. intros [p ?] [q ?] [r ?]; apply Qp_to_Qc_inj_iff, Qcplus_assoc. Qed.
-Global Instance Qp_add_comm : Comm (=) Qp_add.
-Proof. intros [p ?] [q ?]; apply Qp_to_Qc_inj_iff, Qcplus_comm. Qed.
-Global Instance Qp_add_inj_r p : Inj (=) (=) (Qp_add p).
-Proof.
-  destruct p as [p ?].
-  intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl. apply (inj (Qcplus p)).
-Qed.
-Global Instance Qp_add_inj_l p : Inj (=) (=) (λ q, q + p).
-Proof.
-  destruct p as [p ?].
-  intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl. apply (inj (λ q, q + p)%Qc).
-Qed.
-
-Global Instance Qp_mul_assoc : Assoc (=) Qp_mul.
-Proof. intros [p ?] [q ?] [r ?]. apply Qp_to_Qc_inj_iff, Qcmult_assoc. Qed.
-Global Instance Qp_mul_comm : Comm (=) Qp_mul.
-Proof. intros [p ?] [q ?]; apply Qp_to_Qc_inj_iff, Qcmult_comm. Qed.
-Global Instance Qp_mul_inj_r p : Inj (=) (=) (Qp_mul p).
-Proof.
-  destruct p as [p ?]. intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl.
-  intros Hpq.
-  apply (anti_symm Qcle); apply (Qcmult_le_mono_pos_l _ _ p); by rewrite ?Hpq.
-Qed.
-Global Instance Qp_mul_inj_l p : Inj (=) (=) (λ q, q * p).
-Proof.
-  intros q1 q2 Hpq. apply (inj (Qp_mul p)). by rewrite !(comm_L Qp_mul p).
-Qed.
-
-Lemma Qp_mul_add_distr_l p q r : p * (q + r) = p * q + p * r.
-Proof. destruct p, q, r; by apply Qp_to_Qc_inj_iff, Qcmult_plus_distr_r. Qed.
-Lemma Qp_mul_add_distr_r p q r : (p + q) * r = p * r + q * r.
-Proof. destruct p, q, r; by apply Qp_to_Qc_inj_iff, Qcmult_plus_distr_l. Qed.
-Lemma Qp_mul_1_l p : 1 * p = p.
-Proof. destruct p; apply Qp_to_Qc_inj_iff, Qcmult_1_l. Qed.
-Lemma Qp_mul_1_r p : p * 1 = p.
-Proof. destruct p; apply Qp_to_Qc_inj_iff, Qcmult_1_r. Qed.
-
-Lemma Qp_1_1 : 1 + 1 = 2.
-Proof. compute_done. Qed.
-Lemma Qp_add_diag p : p + p = 2 * p.
-Proof. by rewrite <-Qp_1_1, Qp_mul_add_distr_r, !Qp_mul_1_l. Qed.
-
-Lemma Qp_mul_inv_l p : /p * p = 1.
-Proof.
-  destruct p as [p ?]; apply Qp_to_Qc_inj_iff; simpl.
-  by rewrite Qcmult_inv_l, Z2Qc_inj_1 by (by apply not_symmetry, Qclt_not_eq).
-Qed.
-Lemma Qp_mul_inv_r p : p * /p = 1.
-Proof. by rewrite (comm_L Qp_mul), Qp_mul_inv_l. Qed.
-Lemma Qp_inv_mul_distr p q : /(p * q) = /p * /q.
-Proof.
-  apply (inj (Qp_mul (p * q))).
-  rewrite Qp_mul_inv_r, (comm_L Qp_mul p), <-(assoc_L _), (assoc_L Qp_mul p).
-  by rewrite Qp_mul_inv_r, Qp_mul_1_l, Qp_mul_inv_r.
-Qed.
-Lemma Qp_inv_involutive p : / /p = p.
-Proof.
-  rewrite <-(Qp_mul_1_l (/ /p)), <-(Qp_mul_inv_r p), <-(assoc_L _).
-  by rewrite Qp_mul_inv_r, Qp_mul_1_r.
-Qed.
-Global Instance Qp_inv_inj : Inj (=) (=) Qp_inv.
-Proof.
-  intros p1 p2 Hp. apply (inj (Qp_mul (/p1))).
-  by rewrite Qp_mul_inv_l, Hp, Qp_mul_inv_l.
-Qed.
-Lemma Qp_inv_1 : /1 = 1.
-Proof. compute_done. Qed.
-Lemma Qp_inv_half_half : /2 + /2 = 1.
-Proof. compute_done. Qed.
-Lemma Qp_inv_quarter_quarter : /4 + /4 = /2.
-Proof. compute_done. Qed.
-
-Lemma Qp_div_diag p : p / p = 1.
-Proof. apply Qp_mul_inv_r. Qed.
-Lemma Qp_mul_div_l p q : (p / q) * q = p.
-Proof. unfold Qp_div. by rewrite <-(assoc_L _), Qp_mul_inv_l, Qp_mul_1_r. Qed.
-Lemma Qp_mul_div_r p q : q * (p / q) = p.
-Proof. by rewrite (comm_L Qp_mul q), Qp_mul_div_l. Qed.
-Lemma Qp_div_add_distr p q r : (p + q) / r = p / r + q / r.
-Proof. apply Qp_mul_add_distr_r. Qed.
-Lemma Qp_div_div p q r : (p / q) / r = p / (q * r).
-Proof. unfold Qp_div. by rewrite Qp_inv_mul_distr, (assoc_L _). Qed.
-Lemma Qp_div_mul_cancel_l p q r : (r * p) / (r * q) = p / q.
-Proof.
-  rewrite <-Qp_div_div. f_equiv. unfold Qp_div.
-  by rewrite (comm_L Qp_mul r), <-(assoc_L _), Qp_mul_inv_r, Qp_mul_1_r.
-Qed.
-Lemma Qp_div_mul_cancel_r p q r : (p * r) / (q * r) = p / q.
-Proof. by rewrite <-!(comm_L Qp_mul r), Qp_div_mul_cancel_l. Qed.
-Lemma Qp_div_1 p : p / 1 = p.
-Proof. by rewrite <-(Qp_mul_1_r (p / 1)), Qp_mul_div_l. Qed.
-Lemma Qp_div_2 p : p / 2 + p / 2 = p.
-Proof.
-  rewrite <-Qp_div_add_distr, Qp_add_diag.
-  rewrite <-(Qp_mul_1_r 2) at 2. by rewrite Qp_div_mul_cancel_l, Qp_div_1.
-Qed.
-Lemma Qp_div_2_mul p q : p / (2 * q) + p / (2 * q) = p / q.
-Proof. by rewrite <-Qp_div_add_distr, Qp_add_diag, Qp_div_mul_cancel_l. Qed.
-Lemma Qp_half_half : 1 / 2 + 1 / 2 = 1.
-Proof. compute_done. Qed.
-Lemma Qp_quarter_quarter : 1 / 4 + 1 / 4 = 1 / 2.
-Proof. compute_done. Qed.
-Lemma Qp_quarter_three_quarter : 1 / 4 + 3 / 4 = 1.
-Proof. compute_done. Qed.
-Lemma Qp_three_quarter_quarter : 3 / 4 + 1 / 4 = 1.
-Proof. compute_done. Qed.
-Global Instance Qp_div_inj_r p : Inj (=) (=) (Qp_div p).
-Proof. unfold Qp_div; apply _. Qed.
-Global Instance Qp_div_inj_l p : Inj (=) (=) (λ q, q / p)%Qp.
-Proof. unfold Qp_div; apply _. Qed.
-
-Global Instance Qp_le_po : PartialOrder (≤)%Qp.
-Proof.
-  split; [split|].
-  - intros p. by apply Qp_to_Qc_inj_le.
-  - intros p q r. rewrite !Qp_to_Qc_inj_le. by etrans.
-  - intros p q. rewrite !Qp_to_Qc_inj_le, <-Qp_to_Qc_inj_iff. apply Qcle_antisym.
-Qed.
-Global Instance Qp_lt_strict : StrictOrder (<)%Qp.
-Proof.
-  split.
-  - intros p ?%Qp_to_Qc_inj_lt. by apply (irreflexivity (<)%Qc (Qp_to_Qc p)).
-  - intros p q r. rewrite !Qp_to_Qc_inj_lt. by etrans.
-Qed.
-Global Instance Qp_le_total: Total (≤)%Qp.
-Proof. intros p q. rewrite !Qp_to_Qc_inj_le. apply (total Qcle). Qed.
-
-Lemma Qp_lt_le_incl p q : p < q → p ≤ q.
-Proof. rewrite Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qclt_le_weak. Qed.
-Lemma Qp_le_lteq p q : p ≤ q ↔ p < q ∨ p = q.
-Proof.
-  rewrite Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le, <-Qp_to_Qc_inj_iff. split.
-  - intros [?| ->]%Qcle_lt_or_eq; auto.
-  - intros [?| ->]; auto using Qclt_le_weak.
-Qed.
-Lemma Qp_lt_ge_cases p q : {p < q} + {q ≤ p}.
-Proof.
-  refine (cast_if (Qclt_le_dec (Qp_to_Qc p) (Qp_to_Qc q)%Qc));
-    [by apply Qp_to_Qc_inj_lt|by apply Qp_to_Qc_inj_le].
-Defined.
-Lemma Qp_le_lt_trans p q r : p ≤ q → q < r → p < r.
-Proof. rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qcle_lt_trans. Qed.
-Lemma Qp_lt_le_trans p q r : p < q → q ≤ r → p < r.
-Proof. rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qclt_le_trans. Qed.
-
-Lemma Qp_le_ngt p q : p ≤ q ↔ ¬q < p.
-Proof.
-  rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le.
-  split; auto using Qcle_not_lt, Qcnot_lt_le.
-Qed.
-Lemma Qp_lt_nge p q : p < q ↔ ¬q ≤ p.
-Proof.
-  rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le.
-  split; auto using Qclt_not_le, Qcnot_le_lt.
-Qed.
-
-Lemma Qp_add_le_mono_l p q r : p ≤ q ↔ r + p ≤ r + q.
-Proof. rewrite !Qp_to_Qc_inj_le. destruct p, q, r; apply Qcplus_le_mono_l. Qed.
-Lemma Qp_add_le_mono_r p q r : p ≤ q ↔ p + r ≤ q + r.
-Proof. rewrite !(comm_L Qp_add _ r). apply Qp_add_le_mono_l. Qed.
-Lemma Qp_add_le_mono q p n m : q ≤ n → p ≤ m → q + p ≤ n + m.
-Proof. intros. etrans; [by apply Qp_add_le_mono_l|by apply Qp_add_le_mono_r]. Qed.
-
-Lemma Qp_add_lt_mono_l p q r : p < q ↔ r + p < r + q.
-Proof. by rewrite !Qp_lt_nge, <-Qp_add_le_mono_l. Qed.
-Lemma Qp_add_lt_mono_r p q r : p < q ↔ p + r < q + r.
-Proof. by rewrite !Qp_lt_nge, <-Qp_add_le_mono_r. Qed.
-Lemma Qp_add_lt_mono q p n m : q < n → p < m → q + p < n + m.
-Proof. intros. etrans; [by apply Qp_add_lt_mono_l|by apply Qp_add_lt_mono_r]. Qed.
-
-Lemma Qp_mul_le_mono_l p q r : p ≤ q ↔ r * p ≤ r * q.
-Proof.
-  rewrite !Qp_to_Qc_inj_le. destruct p, q, r; by apply Qcmult_le_mono_pos_l.
-Qed.
-Lemma Qp_mul_le_mono_r p q r : p ≤ q ↔ p * r ≤ q * r.
-Proof. rewrite !(comm_L Qp_mul _ r). apply Qp_mul_le_mono_l. Qed.
-Lemma Qp_mul_le_mono q p n m : q ≤ n → p ≤ m → q * p ≤ n * m.
-Proof. intros. etrans; [by apply Qp_mul_le_mono_l|by apply Qp_mul_le_mono_r]. Qed.
-
-Lemma Qp_mul_lt_mono_l p q r : p < q ↔ r * p < r * q.
-Proof.
-  rewrite !Qp_to_Qc_inj_lt. destruct p, q, r; by apply Qcmult_lt_mono_pos_l.
-Qed.
-Lemma Qp_mul_lt_mono_r p q r : p < q ↔ p * r < q * r.
-Proof. rewrite !(comm_L Qp_mul _ r). apply Qp_mul_lt_mono_l. Qed.
-Lemma Qp_mul_lt_mono q p n m : q < n → p < m → q * p < n * m.
-Proof. intros. etrans; [by apply Qp_mul_lt_mono_l|by apply Qp_mul_lt_mono_r]. Qed.
-
-Lemma Qp_lt_add_l p q : p < p + q.
-Proof.
-  destruct p as [p ?], q as [q ?]. apply Qp_to_Qc_inj_lt; simpl.
-  rewrite <- (Qcplus_0_r p) at 1. by rewrite <-Qcplus_lt_mono_l.
-Qed.
-Lemma Qp_lt_add_r p q : q < p + q.
-Proof. rewrite (comm_L Qp_add). apply Qp_lt_add_l. Qed.
-
-Lemma Qp_not_add_le_l p q : ¬(p + q ≤ p).
-Proof. apply Qp_lt_nge, Qp_lt_add_l. Qed.
-Lemma Qp_not_add_le_r p q : ¬(p + q ≤ q).
-Proof. apply Qp_lt_nge, Qp_lt_add_r. Qed.
-
-Lemma Qp_add_id_free q p : q + p ≠ q.
-Proof. intro Heq. apply (Qp_not_add_le_l q p). by rewrite Heq. Qed.
-
-Lemma Qp_le_add_l p q : p ≤ p + q.
-Proof. apply Qp_lt_le_incl, Qp_lt_add_l. Qed.
-Lemma Qp_le_add_r p q : q ≤ p + q.
-Proof. apply Qp_lt_le_incl, Qp_lt_add_r. Qed.
-
-Lemma Qp_sub_Some p q r : p - q = Some r ↔ p = q + r.
-Proof.
-  destruct p as [p Hp], q as [q Hq], r as [r Hr].
-  unfold Qp_sub, Qp_add; simpl; rewrite <-Qp_to_Qc_inj_iff; simpl. split.
-  - intros; simplify_option_eq. unfold Qcminus.
-    by rewrite (Qcplus_comm p), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l.
-  - intros ->. unfold Qcminus.
-    rewrite <-Qcplus_assoc, (Qcplus_comm r), Qcplus_assoc.
-    rewrite Qcplus_opp_r, Qcplus_0_l. simplify_option_eq; [|done].
-    f_equal. by apply Qp_to_Qc_inj_iff.
-Qed.
-Lemma Qp_lt_sum p q : p < q ↔ ∃ r, q = p + r.
-Proof.
-  destruct p as [p Hp], q as [q Hq]. rewrite Qp_to_Qc_inj_lt; simpl.
-  split.
-  - intros Hlt%Qclt_minus_iff. exists (mk_Qp (q - p) Hlt).
-    apply Qp_to_Qc_inj_iff; simpl. unfold Qcminus.
-    by rewrite (Qcplus_comm q), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l.
-  - intros [[r ?] ?%Qp_to_Qc_inj_iff]; simplify_eq/=.
-    rewrite <-(Qcplus_0_r p) at 1. by apply Qcplus_lt_mono_l.
-Qed.
-
-Lemma Qp_sub_None p q : p - q = None ↔ p ≤ q.
-Proof.
-  rewrite Qp_le_ngt, Qp_lt_sum, eq_None_not_Some.
-  by setoid_rewrite <-Qp_sub_Some.
-Qed.
-Lemma Qp_sub_diag p : p - p = None.
-Proof. by apply Qp_sub_None. Qed.
-Lemma Qp_add_sub p q : (p + q) - q = Some p.
-Proof. apply Qp_sub_Some. by rewrite (comm_L Qp_add). Qed.
-
-Lemma Qp_inv_lt_mono p q : p < q ↔ /q < /p.
-Proof.
-  revert p q. cut (∀ p q, p < q → / q < / p).
-  { intros help p q. split; [apply help|]. intros.
-    rewrite <-(Qp_inv_involutive p), <-(Qp_inv_involutive q). by apply help. }
-  intros p q Hpq. apply (Qp_mul_lt_mono_l _ _ q). rewrite Qp_mul_inv_r.
-  apply (Qp_mul_lt_mono_r _ _ p). rewrite <-(assoc_L _), Qp_mul_inv_l.
-  by rewrite Qp_mul_1_l, Qp_mul_1_r.
-Qed.
-Lemma Qp_inv_le_mono p q : p ≤ q ↔ /q ≤ /p.
-Proof. by rewrite !Qp_le_ngt, Qp_inv_lt_mono. Qed.
-
-Lemma Qp_div_le_mono_l p q r : q ≤ p ↔ r / p ≤ r / q.
-Proof. unfold Qp_div. by rewrite <-Qp_mul_le_mono_l, Qp_inv_le_mono. Qed.
-Lemma Qp_div_le_mono_r p q r : p ≤ q ↔ p / r ≤ q / r.
-Proof. apply Qp_mul_le_mono_r. Qed.
-Lemma Qp_div_lt_mono_l p q r : q < p ↔ r / p < r / q.
-Proof. unfold Qp_div. by rewrite <-Qp_mul_lt_mono_l, Qp_inv_lt_mono. Qed.
-Lemma Qp_div_lt_mono_r p q r : p < q ↔ p / r < q / r.
-Proof. apply Qp_mul_lt_mono_r. Qed.
-
-Lemma Qp_div_lt p q : 1 < q → p / q < p.
-Proof. by rewrite (Qp_div_lt_mono_l _ _ p), Qp_div_1. Qed.
-Lemma Qp_div_le p q : 1 ≤ q → p / q ≤ p.
-Proof. by rewrite (Qp_div_le_mono_l _ _ p), Qp_div_1. Qed.
-
-Lemma Qp_lower_bound q1 q2 : ∃ q q1' q2', q1 = q + q1' ∧ q2 = q + q2'.
-Proof.
-  revert q1 q2. cut (∀ q1 q2 : Qp, q1 ≤ q2 →
-    ∃ q q1' q2', q1 = q + q1' ∧ q2 = q + q2').
-  { intros help q1 q2.
-    destruct (Qp_lt_ge_cases q2 q1) as [Hlt|Hle]; eauto.
-    destruct (help q2 q1) as (q&q1'&q2'&?&?); eauto using Qp_lt_le_incl. }
-  intros q1 q2 Hq. exists (q1 / 2)%Qp, (q1 / 2)%Qp.
-  assert (q1 / 2 < q2) as [q2' ->]%Qp_lt_sum.
-  { eapply Qp_lt_le_trans, Hq. by apply Qp_div_lt. }
-  eexists; split; [|done]. by rewrite Qp_div_2.
-Qed.
-
-Lemma Qp_lower_bound_lt q1 q2 : ∃ q : Qp, q < q1 ∧ q < q2.
-Proof.
-  destruct (Qp_lower_bound q1 q2) as (qmin & q1' & q2' & [-> ->]).
-  exists qmin. split; eapply Qp_lt_sum; eauto.
-Qed.
-
-Lemma Qp_cross_split a b c d :
-  a + b = c + d →
-  ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d.
-Proof.
-  intros H. revert a b c d H. cut (∀ a b c d : Qp,
-    a < c → a + b = c + d →
-    ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d)%Qp.
-  { intros help a b c d Habcd.
-    destruct (Qp_lt_ge_cases a c) as [?|[?| ->]%Qp_le_lteq].
-    - auto.
-    - destruct (help c d a b); [done..|]. naive_solver.
-    - apply (inj (Qp_add a)) in Habcd as ->.
-      destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
-      exists a', q, q, d'. repeat split; done || by rewrite (comm_L Qp_add). }
-  intros a b c d [e ->]%Qp_lt_sum. rewrite <-(assoc_L _). intros ->%(inj (Qp_add a)).
-  destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
-  eexists a', q, (q + e)%Qp, d'; split_and?; [by rewrite (comm_L Qp_add)|..|done].
-  - by rewrite (assoc_L _), (comm_L Qp_add e).
-  - by rewrite (assoc_L _), (comm_L Qp_add a').
-Qed.
-
-Lemma Qp_bounded_split p r : ∃ q1 q2 : Qp, q1 ≤ r ∧ p = q1 + q2.
-Proof.
-  destruct (Qp_lt_ge_cases r p) as [[q ->]%Qp_lt_sum|?].
-  { by exists r, q. }
-  exists (p / 2)%Qp, (p / 2)%Qp; split.
-  + trans p; [|done]. by apply Qp_div_le.
-  + by rewrite Qp_div_2.
-Qed.
-
-Lemma Qp_max_spec q p : (q < p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q).
-Proof.
-  unfold Qp_max.
-  destruct (decide (q ≤ p)) as [[?| ->]%Qp_le_lteq|?]; [by auto..|].
-  right. split; [|done]. by apply Qp_lt_le_incl, Qp_lt_nge.
-Qed.
-
-Lemma Qp_max_spec_le q p : (q ≤ p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q).
-Proof. destruct (Qp_max_spec q p) as [[?%Qp_lt_le_incl?]|]; [left|right]; done. Qed.
-
-Global Instance Qp_max_assoc : Assoc (=) Qp_max.
-Proof.
-  intros q p o. unfold Qp_max. destruct (decide (q ≤ p)), (decide (p ≤ o));
-    try by rewrite ?decide_True by (by etrans).
-  rewrite decide_False by done.
-  by rewrite decide_False by (apply Qp_lt_nge; etrans; by apply Qp_lt_nge).
-Qed.
-Global Instance Qp_max_comm : Comm (=) Qp_max.
-Proof.
-  intros q p.
-  destruct (Qp_max_spec_le q p) as [[?->]|[?->]],
-    (Qp_max_spec_le p q) as [[?->]|[?->]]; done || by apply (anti_symm (≤)).
-Qed.
-
-Lemma Qp_max_id q : q `max` q = q.
-Proof. by destruct (Qp_max_spec q q) as [[_->]|[_->]]. Qed.
-
-Lemma Qp_le_max_l q p : q ≤ q `max` p.
-Proof. unfold Qp_max. by destruct (decide (q ≤ p)). Qed.
-Lemma Qp_le_max_r q p : p ≤ q `max` p.
-Proof. rewrite (comm_L Qp_max q). apply Qp_le_max_l. Qed.
-
-Lemma Qp_max_add q p : q `max` p ≤ q + p.
-Proof.
-  unfold Qp_max.
-  destruct (decide (q ≤ p)); [apply Qp_le_add_r|apply Qp_le_add_l].
-Qed.
-
-Lemma Qp_max_lub_l q p o : q `max` p ≤ o → q ≤ o.
-Proof. unfold Qp_max. destruct (decide (q ≤ p)); [by etrans|done]. Qed.
-Lemma Qp_max_lub_r q p o : q `max` p ≤ o → p ≤ o.
-Proof. rewrite (comm _ q). apply Qp_max_lub_l. Qed.
-
-Lemma Qp_min_spec q p : (q < p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p).
-Proof.
-  unfold Qp_min.
-  destruct (decide (q ≤ p)) as [[?| ->]%Qp_le_lteq|?]; [by auto..|].
-  right. split; [|done]. by apply Qp_lt_le_incl, Qp_lt_nge.
-Qed.
-
-Lemma Qp_min_spec_le q p : (q ≤ p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p).
-Proof. destruct (Qp_min_spec q p) as [[?%Qp_lt_le_incl ?]|]; [left|right]; done. Qed.
-
-Global Instance Qp_min_assoc : Assoc (=) Qp_min.
-Proof.
-  intros q p o. unfold Qp_min.
-  destruct (decide (q ≤ p)), (decide (p ≤ o)); eauto using decide_False.
-  - by rewrite !decide_True by (by etrans).
-  - by rewrite decide_False by (apply Qp_lt_nge; etrans; by apply Qp_lt_nge).
-Qed.
-Global Instance Qp_min_comm : Comm (=) Qp_min.
-Proof.
-  intros q p.
-  destruct (Qp_min_spec_le q p) as [[?->]|[?->]],
-    (Qp_min_spec_le p q) as [[? ->]|[? ->]]; done || by apply (anti_symm (≤)).
-Qed.
-
-Lemma Qp_min_id q : q `min` q = q.
-Proof. by destruct (Qp_min_spec q q) as [[_->]|[_->]]. Qed.
-Lemma Qp_le_min_r q p : q `min` p ≤ p.
-Proof. by destruct (Qp_min_spec_le q p) as [[?->]|[?->]]. Qed.
-
-Lemma Qp_le_min_l p q : p `min` q ≤ p.
-Proof. rewrite (comm_L Qp_min p). apply Qp_le_min_r. Qed.
+Local Open Scope Qp_scope.
 
-Lemma Qp_min_l_iff q p : q `min` p = q ↔ q ≤ p.
-Proof.
-  destruct (Qp_min_spec_le q p) as [[?->]|[?->]]; [done|].
-  split; [by intros ->|]. intros. by apply (anti_symm (≤)).
-Qed.
-Lemma Qp_min_r_iff q p : q `min` p = p ↔ p ≤ q.
-Proof. rewrite (comm_L Qp_min q). apply Qp_min_l_iff. Qed.
+Module Qp.
+  Lemma to_Qc_inj_iff p q : Qp_to_Qc p = Qp_to_Qc q ↔ p = q.
+  Proof.
+    split; [|by intros ->].
+    destruct p, q; intros; simplify_eq/=; f_equal; apply (proof_irrel _).
+  Qed.
+  Global Instance eq_dec : EqDecision Qp.
+  Proof.
+    refine (λ p q, cast_if (decide (Qp_to_Qc p = Qp_to_Qc q)));
+      by rewrite <-to_Qc_inj_iff.
+  Defined.
+
+  Definition add (p q : Qp) : Qp :=
+    let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
+    mk_Qp (p + q) (Qcplus_pos_pos _ _ Hp Hq).
+  Global Arguments add : simpl never.
+
+  Definition sub (p q : Qp) : option Qp :=
+    let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
+    let pq := (p - q)%Qc in
+    guard (0 < pq)%Qc as Hpq; Some (mk_Qp pq Hpq).
+  Global Arguments sub : simpl never.
+
+  Definition mul (p q : Qp) : Qp :=
+    let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
+    mk_Qp (p * q) (Qcmult_pos_pos _ _ Hp Hq).
+  Global Arguments mul : simpl never.
+
+  Definition inv (q : Qp) : Qp :=
+    let 'mk_Qp q Hq := q return _ in
+    mk_Qp (/ q)%Qc (Qcinv_pos _ Hq).
+  Global Arguments inv : simpl never.
+
+  Definition div (p q : Qp) : Qp := mul p (inv q).
+  Typeclasses Opaque div.
+  Global Arguments div : simpl never.
+
+  Definition le (p q : Qp) : Prop :=
+    let 'mk_Qp p _ := p in let 'mk_Qp q _ := q in (p ≤ q)%Qc.
+  Definition lt (p q : Qp) : Prop :=
+    let 'mk_Qp p _ := p in let 'mk_Qp q _ := q in (p < q)%Qc.
+
+  Lemma to_Qc_inj_add p q : Qp_to_Qc (add p q) = (Qp_to_Qc p + Qp_to_Qc q)%Qc.
+  Proof. by destruct p, q. Qed.
+  Lemma to_Qc_inj_mul p q : Qp_to_Qc (mul p q) = (Qp_to_Qc p * Qp_to_Qc q)%Qc.
+  Proof. by destruct p, q. Qed.
+  Lemma to_Qc_inj_le p q : le p q ↔ (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc.
+  Proof. by destruct p, q. Qed.
+  Lemma to_Qc_inj_lt p q : lt p q ↔ (Qp_to_Qc p < Qp_to_Qc q)%Qc.
+  Proof. by destruct p, q. Qed.
+
+  Global Instance le_dec : RelDecision le.
+  Proof.
+    refine (λ p q, cast_if (decide (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc));
+      by rewrite to_Qc_inj_le.
+  Qed.
+  Global Instance lt_dec : RelDecision lt.
+  Proof.
+    refine (λ p q, cast_if (decide (Qp_to_Qc p < Qp_to_Qc q)%Qc));
+      by rewrite to_Qc_inj_lt.
+  Qed.
+  Global Instance lt_pi p q : ProofIrrel (lt p q).
+  Proof. destruct p, q; apply _. Qed.
+
+  Definition max (q p : Qp) : Qp := if decide (le q p) then p else q.
+  Definition min (q p : Qp) : Qp := if decide (le q p) then q else p.
+
+  Module Import notations.
+    Infix "+" := add : Qp_scope.
+    Infix "-" := sub : Qp_scope.
+    Infix "*" := mul : Qp_scope.
+    Notation "/ q" := (inv q) : Qp_scope.
+    Infix "/" := div : Qp_scope.
+
+    Notation "1" := (pos_to_Qp 1) : Qp_scope.
+    Notation "2" := (pos_to_Qp 2) : Qp_scope.
+    Notation "3" := (pos_to_Qp 3) : Qp_scope.
+    Notation "4" := (pos_to_Qp 4) : Qp_scope.
+
+    Infix "≤" := le : Qp_scope.
+    Infix "<" := lt : Qp_scope.
+    Notation "p ≤ q ≤ r" := (p ≤ q ∧ q ≤ r) : Qp_scope.
+    Notation "p ≤ q < r" := (p ≤ q ∧ q < r) : Qp_scope.
+    Notation "p < q < r" := (p < q ∧ q < r) : Qp_scope.
+    Notation "p < q ≤ r" := (p < q ∧ q ≤ r) : Qp_scope.
+    Notation "p ≤ q ≤ r ≤ r'" := (p ≤ q ∧ q ≤ r ∧ r ≤ r') : Qp_scope.
+    Notation "(≤)" := le (only parsing) : Qp_scope.
+    Notation "(<)" := lt (only parsing) : Qp_scope.
+
+    Infix "`max`" := max : Qp_scope.
+    Infix "`min`" := min : Qp_scope.
+  End notations.
+
+  Global Hint Extern 0 (_ ≤ _)%Qp => reflexivity : core.
+
+  Global Instance inhabited : Inhabited Qp := populate 1.
+
+  Global Instance add_assoc : Assoc (=) add.
+  Proof. intros [p ?] [q ?] [r ?]; apply to_Qc_inj_iff, Qcplus_assoc. Qed.
+  Global Instance add_comm : Comm (=) add.
+  Proof. intros [p ?] [q ?]; apply to_Qc_inj_iff, Qcplus_comm. Qed.
+  Global Instance add_inj_r p : Inj (=) (=) (add p).
+  Proof.
+    destruct p as [p ?].
+    intros [q1 ?] [q2 ?]. rewrite <-!to_Qc_inj_iff; simpl. apply (inj (Qcplus p)).
+  Qed.
+  Global Instance add_inj_l p : Inj (=) (=) (λ q, q + p).
+  Proof.
+    destruct p as [p ?].
+    intros [q1 ?] [q2 ?]. rewrite <-!to_Qc_inj_iff; simpl. apply (inj (λ q, q + p)%Qc).
+  Qed.
+
+  Global Instance mul_assoc : Assoc (=) mul.
+  Proof. intros [p ?] [q ?] [r ?]. apply Qp.to_Qc_inj_iff, Qcmult_assoc. Qed.
+  Global Instance mul_comm : Comm (=) mul.
+  Proof. intros [p ?] [q ?]; apply Qp.to_Qc_inj_iff, Qcmult_comm. Qed.
+  Global Instance mul_inj_r p : Inj (=) (=) (mul p).
+  Proof.
+    destruct p as [p ?]. intros [q1 ?] [q2 ?]. rewrite <-!Qp.to_Qc_inj_iff; simpl.
+    intros Hpq.
+    apply (anti_symm Qcle); apply (Qcmult_le_mono_pos_l _ _ p); by rewrite ?Hpq.
+  Qed.
+  Global Instance mul_inj_l p : Inj (=) (=) (λ q, q * p).
+  Proof.
+    intros q1 q2 Hpq. apply (inj (mul p)). by rewrite !(comm_L mul p).
+  Qed.
+
+  Lemma mul_add_distr_l p q r : p * (q + r) = p * q + p * r.
+  Proof. destruct p, q, r; by apply Qp.to_Qc_inj_iff, Qcmult_plus_distr_r. Qed.
+  Lemma mul_add_distr_r p q r : (p + q) * r = p * r + q * r.
+  Proof. destruct p, q, r; by apply Qp.to_Qc_inj_iff, Qcmult_plus_distr_l. Qed.
+  Lemma mul_1_l p : 1 * p = p.
+  Proof. destruct p; apply Qp.to_Qc_inj_iff, Qcmult_1_l. Qed.
+  Lemma mul_1_r p : p * 1 = p.
+  Proof. destruct p; apply Qp.to_Qc_inj_iff, Qcmult_1_r. Qed.
+
+  Lemma add_1_1 : 1 + 1 = 2.
+  Proof. compute_done. Qed.
+  Lemma add_diag p : p + p = 2 * p.
+  Proof. by rewrite <-add_1_1, mul_add_distr_r, !mul_1_l. Qed.
+
+  Lemma mul_inv_l p : /p * p = 1.
+  Proof.
+    destruct p as [p ?]; apply Qp.to_Qc_inj_iff; simpl.
+    by rewrite Qcmult_inv_l, Z2Qc_inj_1 by (by apply not_symmetry, Qclt_not_eq).
+  Qed.
+  Lemma mul_inv_r p : p * /p = 1.
+  Proof. by rewrite (comm_L mul), mul_inv_l. Qed.
+  Lemma inv_mul_distr p q : /(p * q) = /p * /q.
+  Proof.
+    apply (inj (mul (p * q))).
+    rewrite mul_inv_r, (comm_L mul p), <-(assoc_L _), (assoc_L mul p).
+    by rewrite mul_inv_r, mul_1_l, mul_inv_r.
+  Qed.
+  Lemma inv_involutive p : / /p = p.
+  Proof.
+    rewrite <-(mul_1_l (/ /p)), <-(mul_inv_r p), <-(assoc_L _).
+    by rewrite mul_inv_r, mul_1_r.
+  Qed.
+  Global Instance inv_inj : Inj (=) (=) inv.
+  Proof.
+    intros p1 p2 Hp. apply (inj (mul (/p1))).
+    by rewrite mul_inv_l, Hp, mul_inv_l.
+  Qed.
+  Lemma inv_1 : /1 = 1.
+  Proof. compute_done. Qed.
+  Lemma inv_half_half : /2 + /2 = 1.
+  Proof. compute_done. Qed.
+  Lemma inv_quarter_quarter : /4 + /4 = /2.
+  Proof. compute_done. Qed.
+
+  Lemma div_diag p : p / p = 1.
+  Proof. apply mul_inv_r. Qed.
+  Lemma mul_div_l p q : (p / q) * q = p.
+  Proof. unfold div. by rewrite <-(assoc_L _), mul_inv_l, mul_1_r. Qed.
+  Lemma mul_div_r p q : q * (p / q) = p.
+  Proof. by rewrite (comm_L mul q), mul_div_l. Qed.
+  Lemma div_add_distr p q r : (p + q) / r = p / r + q / r.
+  Proof. apply mul_add_distr_r. Qed.
+  Lemma div_div p q r : (p / q) / r = p / (q * r).
+  Proof. unfold div. by rewrite inv_mul_distr, (assoc_L _). Qed.
+  Lemma div_mul_cancel_l p q r : (r * p) / (r * q) = p / q.
+  Proof.
+    rewrite <-div_div. f_equiv. unfold div.
+    by rewrite (comm_L mul r), <-(assoc_L _), mul_inv_r, mul_1_r.
+  Qed.
+  Lemma div_mul_cancel_r p q r : (p * r) / (q * r) = p / q.
+  Proof. by rewrite <-!(comm_L mul r), div_mul_cancel_l. Qed.
+  Lemma div_1 p : p / 1 = p.
+  Proof. by rewrite <-(mul_1_r (p / 1)), mul_div_l. Qed.
+  Lemma div_2 p : p / 2 + p / 2 = p.
+  Proof.
+    rewrite <-div_add_distr, add_diag.
+    rewrite <-(mul_1_r 2) at 2. by rewrite div_mul_cancel_l, div_1.
+  Qed.
+  Lemma div_2_mul p q : p / (2 * q) + p / (2 * q) = p / q.
+  Proof. by rewrite <-div_add_distr, add_diag, div_mul_cancel_l. Qed.
+
+  Lemma half_half : 1 / 2 + 1 / 2 = 1.
+  Proof. compute_done. Qed.
+  Lemma quarter_quarter : 1 / 4 + 1 / 4 = 1 / 2.
+  Proof. compute_done. Qed.
+  Lemma quarter_three_quarter : 1 / 4 + 3 / 4 = 1.
+  Proof. compute_done. Qed.
+  Lemma three_quarter_quarter : 3 / 4 + 1 / 4 = 1.
+  Proof. compute_done. Qed.
+
+  Global Instance div_inj_r p : Inj (=) (=) (div p).
+  Proof. unfold div; apply _. Qed.
+  Global Instance div_inj_l p : Inj (=) (=) (λ q, q / p)%Qp.
+  Proof. unfold div; apply _. Qed.
+
+  Global Instance le_po : PartialOrder (≤).
+  Proof.
+    split; [split|].
+    - intros p. by apply to_Qc_inj_le.
+    - intros p q r. rewrite !to_Qc_inj_le. by etrans.
+    - intros p q. rewrite !to_Qc_inj_le, <-to_Qc_inj_iff. apply Qcle_antisym.
+  Qed.
+  Global Instance lt_strict : StrictOrder (<).
+  Proof.
+    split.
+    - intros p ?%to_Qc_inj_lt. by apply (irreflexivity (<)%Qc (Qp_to_Qc p)).
+    - intros p q r. rewrite !to_Qc_inj_lt. by etrans.
+  Qed.
+  Global Instance le_total: Total (≤).
+  Proof. intros p q. rewrite !to_Qc_inj_le. apply (total Qcle). Qed.
+
+  Lemma lt_le_incl p q : p < q → p ≤ q.
+  Proof. rewrite to_Qc_inj_lt, to_Qc_inj_le. apply Qclt_le_weak. Qed.
+  Lemma le_lteq p q : p ≤ q ↔ p < q ∨ p = q.
+  Proof.
+    rewrite to_Qc_inj_lt, to_Qc_inj_le, <-Qp.to_Qc_inj_iff. split.
+    - intros [?| ->]%Qcle_lt_or_eq; auto.
+    - intros [?| ->]; auto using Qclt_le_weak.
+  Qed.
+  Lemma lt_ge_cases p q : {p < q} + {q ≤ p}.
+  Proof.
+    refine (cast_if (Qclt_le_dec (Qp_to_Qc p) (Qp_to_Qc q)%Qc));
+      [by apply to_Qc_inj_lt|by apply to_Qc_inj_le].
+  Defined.
+  Lemma le_lt_trans p q r : p ≤ q → q < r → p < r.
+  Proof. rewrite !to_Qc_inj_lt, to_Qc_inj_le. apply Qcle_lt_trans. Qed.
+  Lemma lt_le_trans p q r : p < q → q ≤ r → p < r.
+  Proof. rewrite !to_Qc_inj_lt, to_Qc_inj_le. apply Qclt_le_trans. Qed.
+
+  Lemma le_ngt p q : p ≤ q ↔ ¬q < p.
+  Proof.
+    rewrite !to_Qc_inj_lt, to_Qc_inj_le.
+    split; auto using Qcle_not_lt, Qcnot_lt_le.
+  Qed.
+  Lemma lt_nge p q : p < q ↔ ¬q ≤ p.
+  Proof.
+    rewrite !to_Qc_inj_lt, to_Qc_inj_le.
+    split; auto using Qclt_not_le, Qcnot_le_lt.
+  Qed.
+
+  Lemma add_le_mono_l p q r : p ≤ q ↔ r + p ≤ r + q.
+  Proof. rewrite !to_Qc_inj_le. destruct p, q, r; apply Qcplus_le_mono_l. Qed.
+  Lemma add_le_mono_r p q r : p ≤ q ↔ p + r ≤ q + r.
+  Proof. rewrite !(comm_L add _ r). apply add_le_mono_l. Qed.
+  Lemma add_le_mono q p n m : q ≤ n → p ≤ m → q + p ≤ n + m.
+  Proof. intros. etrans; [by apply add_le_mono_l|by apply add_le_mono_r]. Qed.
+
+  Lemma add_lt_mono_l p q r : p < q ↔ r + p < r + q.
+  Proof. by rewrite !lt_nge, <-add_le_mono_l. Qed.
+  Lemma add_lt_mono_r p q r : p < q ↔ p + r < q + r.
+  Proof. by rewrite !lt_nge, <-add_le_mono_r. Qed.
+  Lemma add_lt_mono q p n m : q < n → p < m → q + p < n + m.
+  Proof. intros. etrans; [by apply add_lt_mono_l|by apply add_lt_mono_r]. Qed.
+
+  Lemma mul_le_mono_l p q r : p ≤ q ↔ r * p ≤ r * q.
+  Proof.
+    rewrite !to_Qc_inj_le. destruct p, q, r; by apply Qcmult_le_mono_pos_l.
+  Qed.
+  Lemma mul_le_mono_r p q r : p ≤ q ↔ p * r ≤ q * r.
+  Proof. rewrite !(comm_L mul _ r). apply mul_le_mono_l. Qed.
+  Lemma mul_le_mono q p n m : q ≤ n → p ≤ m → q * p ≤ n * m.
+  Proof. intros. etrans; [by apply mul_le_mono_l|by apply mul_le_mono_r]. Qed.
+
+  Lemma mul_lt_mono_l p q r : p < q ↔ r * p < r * q.
+  Proof.
+    rewrite !to_Qc_inj_lt. destruct p, q, r; by apply Qcmult_lt_mono_pos_l.
+  Qed.
+  Lemma mul_lt_mono_r p q r : p < q ↔ p * r < q * r.
+  Proof. rewrite !(comm_L mul _ r). apply mul_lt_mono_l. Qed.
+  Lemma mul_lt_mono q p n m : q < n → p < m → q * p < n * m.
+  Proof. intros. etrans; [by apply mul_lt_mono_l|by apply mul_lt_mono_r]. Qed.
+
+  Lemma lt_add_l p q : p < p + q.
+  Proof.
+    destruct p as [p ?], q as [q ?]. apply to_Qc_inj_lt; simpl.
+    rewrite <- (Qcplus_0_r p) at 1. by rewrite <-Qcplus_lt_mono_l.
+  Qed.
+  Lemma lt_add_r p q : q < p + q.
+  Proof. rewrite (comm_L add). apply lt_add_l. Qed.
+
+  Lemma not_add_le_l p q : ¬(p + q ≤ p).
+  Proof. apply lt_nge, lt_add_l. Qed.
+  Lemma not_add_le_r p q : ¬(p + q ≤ q).
+  Proof. apply lt_nge, lt_add_r. Qed.
+
+  Lemma add_id_free q p : q + p ≠ q.
+  Proof. intro Heq. apply (not_add_le_l q p). by rewrite Heq. Qed.
+
+  Lemma le_add_l p q : p ≤ p + q.
+  Proof. apply lt_le_incl, lt_add_l. Qed.
+  Lemma le_add_r p q : q ≤ p + q.
+  Proof. apply lt_le_incl, lt_add_r. Qed.
+
+  Lemma sub_Some p q r : p - q = Some r ↔ p = q + r.
+  Proof.
+    destruct p as [p Hp], q as [q Hq], r as [r Hr].
+    unfold sub, add; simpl; rewrite <-Qp.to_Qc_inj_iff; simpl. split.
+    - intros; simplify_option_eq. unfold Qcminus.
+      by rewrite (Qcplus_comm p), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l.
+    - intros ->. unfold Qcminus.
+      rewrite <-Qcplus_assoc, (Qcplus_comm r), Qcplus_assoc.
+      rewrite Qcplus_opp_r, Qcplus_0_l. simplify_option_eq; [|done].
+      f_equal. by apply Qp.to_Qc_inj_iff.
+  Qed.
+  Lemma lt_sum p q : p < q ↔ ∃ r, q = p + r.
+  Proof.
+    destruct p as [p Hp], q as [q Hq]. rewrite to_Qc_inj_lt; simpl.
+    split.
+    - intros Hlt%Qclt_minus_iff. exists (mk_Qp (q - p) Hlt).
+      apply Qp.to_Qc_inj_iff; simpl. unfold Qcminus.
+      by rewrite (Qcplus_comm q), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l.
+    - intros [[r ?] ?%Qp.to_Qc_inj_iff]; simplify_eq/=.
+      rewrite <-(Qcplus_0_r p) at 1. by apply Qcplus_lt_mono_l.
+  Qed.
+
+  Lemma sub_None p q : p - q = None ↔ p ≤ q.
+  Proof.
+    rewrite le_ngt, lt_sum, eq_None_not_Some.
+    by setoid_rewrite <-sub_Some.
+  Qed.
+  Lemma sub_diag p : p - p = None.
+  Proof. by apply sub_None. Qed.
+  Lemma add_sub p q : (p + q) - q = Some p.
+  Proof. apply sub_Some. by rewrite (comm_L add). Qed.
+
+  Lemma inv_lt_mono p q : p < q ↔ /q < /p.
+  Proof.
+    revert p q. cut (∀ p q, p < q → / q < / p).
+    { intros help p q. split; [apply help|]. intros.
+      rewrite <-(inv_involutive p), <-(inv_involutive q). by apply help. }
+    intros p q Hpq. apply (mul_lt_mono_l _ _ q). rewrite mul_inv_r.
+    apply (mul_lt_mono_r _ _ p). rewrite <-(assoc_L _), mul_inv_l.
+    by rewrite mul_1_l, mul_1_r.
+  Qed.
+  Lemma inv_le_mono p q : p ≤ q ↔ /q ≤ /p.
+  Proof. by rewrite !le_ngt, inv_lt_mono. Qed.
+
+  Lemma div_le_mono_l p q r : q ≤ p ↔ r / p ≤ r / q.
+  Proof. unfold div. by rewrite <-mul_le_mono_l, inv_le_mono. Qed.
+  Lemma div_le_mono_r p q r : p ≤ q ↔ p / r ≤ q / r.
+  Proof. apply mul_le_mono_r. Qed.
+  Lemma div_lt_mono_l p q r : q < p ↔ r / p < r / q.
+  Proof. unfold div. by rewrite <-mul_lt_mono_l, inv_lt_mono. Qed.
+  Lemma div_lt_mono_r p q r : p < q ↔ p / r < q / r.
+  Proof. apply mul_lt_mono_r. Qed.
+
+  Lemma div_lt p q : 1 < q → p / q < p.
+  Proof. by rewrite (div_lt_mono_l _ _ p), div_1. Qed.
+  Lemma div_le p q : 1 ≤ q → p / q ≤ p.
+  Proof. by rewrite (div_le_mono_l _ _ p), div_1. Qed.
+
+  Lemma lower_bound q1 q2 : ∃ q q1' q2', q1 = q + q1' ∧ q2 = q + q2'.
+  Proof.
+    revert q1 q2. cut (∀ q1 q2 : Qp, q1 ≤ q2 →
+      ∃ q q1' q2', q1 = q + q1' ∧ q2 = q + q2').
+    { intros help q1 q2.
+      destruct (lt_ge_cases q2 q1) as [Hlt|Hle]; eauto.
+      destruct (help q2 q1) as (q&q1'&q2'&?&?); eauto using lt_le_incl. }
+    intros q1 q2 Hq. exists (q1 / 2)%Qp, (q1 / 2)%Qp.
+    assert (q1 / 2 < q2) as [q2' ->]%lt_sum.
+    { eapply lt_le_trans, Hq. by apply div_lt. }
+    eexists; split; [|done]. by rewrite div_2.
+  Qed.
+
+  Lemma lower_bound_lt q1 q2 : ∃ q : Qp, q < q1 ∧ q < q2.
+  Proof.
+    destruct (lower_bound q1 q2) as (qmin & q1' & q2' & [-> ->]).
+    exists qmin. split; eapply lt_sum; eauto.
+  Qed.
+
+  Lemma cross_split a b c d :
+    a + b = c + d →
+    ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d.
+  Proof.
+    intros H. revert a b c d H. cut (∀ a b c d : Qp,
+      a < c → a + b = c + d →
+      ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d)%Qp.
+    { intros help a b c d Habcd.
+      destruct (lt_ge_cases a c) as [?|[?| ->]%le_lteq].
+      - auto.
+      - destruct (help c d a b); [done..|]. naive_solver.
+      - apply (inj (add a)) in Habcd as ->.
+        destruct (lower_bound a d) as (q&a'&d'&->&->).
+        exists a', q, q, d'. repeat split; done || by rewrite (comm_L add). }
+    intros a b c d [e ->]%lt_sum. rewrite <-(assoc_L _). intros ->%(inj (add a)).
+    destruct (lower_bound a d) as (q&a'&d'&->&->).
+    eexists a', q, (q + e)%Qp, d'; split_and?; [by rewrite (comm_L add)|..|done].
+    - by rewrite (assoc_L _), (comm_L add e).
+    - by rewrite (assoc_L _), (comm_L add a').
+  Qed.
+
+  Lemma bounded_split p r : ∃ q1 q2 : Qp, q1 ≤ r ∧ p = q1 + q2.
+  Proof.
+    destruct (lt_ge_cases r p) as [[q ->]%lt_sum|?].
+    { by exists r, q. }
+    exists (p / 2)%Qp, (p / 2)%Qp; split.
+    + trans p; [|done]. by apply div_le.
+    + by rewrite div_2.
+  Qed.
+
+  Lemma max_spec q p : (q < p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q).
+  Proof.
+    unfold max.
+    destruct (decide (q ≤ p)) as [[?| ->]%le_lteq|?]; [by auto..|].
+    right. split; [|done]. by apply lt_le_incl, lt_nge.
+  Qed.
+
+  Lemma max_spec_le q p : (q ≤ p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q).
+  Proof. destruct (max_spec q p) as [[?%lt_le_incl?]|]; [left|right]; done. Qed.
+
+  Global Instance max_assoc : Assoc (=) max.
+  Proof.
+    intros q p o. unfold max. destruct (decide (q ≤ p)), (decide (p ≤ o));
+      try by rewrite ?decide_True by (by etrans).
+    rewrite decide_False by done.
+    by rewrite decide_False by (apply lt_nge; etrans; by apply lt_nge).
+  Qed.
+  Global Instance max_comm : Comm (=) max.
+  Proof.
+    intros q p.
+    destruct (max_spec_le q p) as [[?->]|[?->]],
+      (max_spec_le p q) as [[?->]|[?->]]; done || by apply (anti_symm (≤)).
+  Qed.
+
+  Lemma max_id q : q `max` q = q.
+  Proof. by destruct (max_spec q q) as [[_->]|[_->]]. Qed.
+
+  Lemma le_max_l q p : q ≤ q `max` p.
+  Proof. unfold max. by destruct (decide (q ≤ p)). Qed.
+  Lemma le_max_r q p : p ≤ q `max` p.
+  Proof. rewrite (comm_L max q). apply le_max_l. Qed.
+
+  Lemma max_add q p : q `max` p ≤ q + p.
+  Proof.
+    unfold max.
+    destruct (decide (q ≤ p)); [apply le_add_r|apply le_add_l].
+  Qed.
+
+  Lemma max_lub_l q p o : q `max` p ≤ o → q ≤ o.
+  Proof. unfold max. destruct (decide (q ≤ p)); [by etrans|done]. Qed.
+  Lemma max_lub_r q p o : q `max` p ≤ o → p ≤ o.
+  Proof. rewrite (comm _ q). apply max_lub_l. Qed.
+
+  Lemma min_spec q p : (q < p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p).
+  Proof.
+    unfold min.
+    destruct (decide (q ≤ p)) as [[?| ->]%le_lteq|?]; [by auto..|].
+    right. split; [|done]. by apply lt_le_incl, lt_nge.
+  Qed.
+
+  Lemma min_spec_le q p : (q ≤ p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p).
+  Proof. destruct (min_spec q p) as [[?%lt_le_incl ?]|]; [left|right]; done. Qed.
+
+  Global Instance min_assoc : Assoc (=) min.
+  Proof.
+    intros q p o. unfold min.
+    destruct (decide (q ≤ p)), (decide (p ≤ o)); eauto using decide_False.
+    - by rewrite !decide_True by (by etrans).
+    - by rewrite decide_False by (apply lt_nge; etrans; by apply lt_nge).
+  Qed.
+  Global Instance min_comm : Comm (=) min.
+  Proof.
+    intros q p.
+    destruct (min_spec_le q p) as [[?->]|[?->]],
+      (min_spec_le p q) as [[? ->]|[? ->]]; done || by apply (anti_symm (≤)).
+  Qed.
+
+  Lemma min_id q : q `min` q = q.
+  Proof. by destruct (min_spec q q) as [[_->]|[_->]]. Qed.
+  Lemma le_min_r q p : q `min` p ≤ p.
+  Proof. by destruct (min_spec_le q p) as [[?->]|[?->]]. Qed.
+
+  Lemma le_min_l p q : p `min` q ≤ p.
+  Proof. rewrite (comm_L min p). apply le_min_r. Qed.
+
+  Lemma min_l_iff q p : q `min` p = q ↔ q ≤ p.
+  Proof.
+    destruct (min_spec_le q p) as [[?->]|[?->]]; [done|].
+    split; [by intros ->|]. intros. by apply (anti_symm (≤)).
+  Qed.
+  Lemma min_r_iff q p : q `min` p = p ↔ p ≤ q.
+  Proof. rewrite (comm_L min q). apply min_l_iff. Qed.
+End Qp.
+
+Export Qp.notations.
 
 Lemma pos_to_Qp_1 : pos_to_Qp 1 = 1.
 Proof. compute_done. Qed.
@@ -1266,13 +1346,13 @@ Proof. by injection 1. Qed.
 Lemma pos_to_Qp_inj_iff n m : pos_to_Qp n = pos_to_Qp m ↔ n = m.
 Proof. split; [apply pos_to_Qp_inj|by intros ->]. Qed.
 Lemma pos_to_Qp_inj_le n m : (n ≤ m)%positive ↔ pos_to_Qp n ≤ pos_to_Qp m.
-Proof. rewrite Qp_to_Qc_inj_le; simpl. by rewrite <-Z2Qc_inj_le. Qed.
+Proof. rewrite Qp.to_Qc_inj_le; simpl. by rewrite <-Z2Qc_inj_le. Qed.
 Lemma pos_to_Qp_inj_lt n m : (n < m)%positive ↔ pos_to_Qp n < pos_to_Qp m.
-Proof. by rewrite Pos.lt_nle, Qp_lt_nge, <-pos_to_Qp_inj_le. Qed.
+Proof. by rewrite Pos.lt_nle, Qp.lt_nge, <-pos_to_Qp_inj_le. Qed.
 Lemma pos_to_Qp_add x y : pos_to_Qp x + pos_to_Qp y = pos_to_Qp (x + y).
-Proof. apply Qp_to_Qc_inj_iff; simpl. by rewrite Pos2Z.inj_add, Z2Qc_inj_add. Qed.
+Proof. apply Qp.to_Qc_inj_iff; simpl. by rewrite Pos2Z.inj_add, Z2Qc_inj_add. Qed.
 Lemma pos_to_Qp_mul x y : pos_to_Qp x * pos_to_Qp y = pos_to_Qp (x * y).
-Proof. apply Qp_to_Qc_inj_iff; simpl. by rewrite Pos2Z.inj_mul, Z2Qc_inj_mul. Qed.
+Proof. apply Qp.to_Qc_inj_iff; simpl. by rewrite Pos2Z.inj_mul, Z2Qc_inj_mul. Qed.
 
 Local Close Scope Qp_scope.
 
@@ -1295,7 +1375,7 @@ Definition rotate_nat_sub (base offset len : nat) : nat :=
 Lemma rotate_nat_add_add_mod base offset len:
   rotate_nat_add base offset len =
   rotate_nat_add (base `mod` len) offset len.
-Proof. unfold rotate_nat_add. by rewrite Nat2Z_inj_mod, Zplus_mod_idemp_l. Qed.
+Proof. unfold rotate_nat_add. by rewrite Nat2Z.inj_mod, Zplus_mod_idemp_l. Qed.
 
 Lemma rotate_nat_add_alt base offset len:
   base < len → offset < len →
@@ -1304,7 +1384,7 @@ Lemma rotate_nat_add_alt base offset len:
 Proof.
   unfold rotate_nat_add. intros ??. case_decide.
   - rewrite Z.mod_small by lia. by rewrite <-Nat2Z.inj_add, Nat2Z.id.
-  - rewrite (Zmod_in_range 1) by lia.
+  - rewrite (Z.mod_in_range 1) by lia.
     by rewrite Z.mul_1_l, <-Nat2Z.inj_add, <-Nat2Z.inj_sub,Nat2Z.id by lia.
 Qed.
 Lemma rotate_nat_sub_alt base offset len:
@@ -1315,7 +1395,7 @@ Proof.
   unfold rotate_nat_sub. intros ??. case_decide.
   - rewrite Z.mod_small by lia.
     by rewrite <-Nat2Z.inj_add, <-Nat2Z.inj_sub, Nat2Z.id by lia.
-  - rewrite (Zmod_in_range 1) by lia.
+  - rewrite (Z.mod_in_range 1) by lia.
     rewrite Z.mul_1_l, <-Nat2Z.inj_add, <-!Nat2Z.inj_sub,Nat2Z.id; lia.
 Qed.
 
@@ -1334,7 +1414,7 @@ Lemma rotate_nat_add_lt base offset len :
 Proof.
   unfold rotate_nat_add. intros ?.
   pose proof (Nat.mod_upper_bound (base + offset) len).
-  rewrite Z2Nat_inj_mod, Z2Nat.inj_add, !Nat2Z.id; lia.
+  rewrite Z2Nat.inj_mod, Z2Nat.inj_add, !Nat2Z.id; lia.
 Qed.
 Lemma rotate_nat_sub_lt base offset len :
   0 < len → rotate_nat_sub base offset len < len.
@@ -1349,10 +1429,10 @@ Lemma rotate_nat_add_sub base len offset:
   rotate_nat_add base (rotate_nat_sub base offset len) len = offset.
 Proof.
   intros ?. unfold rotate_nat_add, rotate_nat_sub.
-  rewrite Z2Nat.id by (apply Z_mod_pos; lia). rewrite Zplus_mod_idemp_r.
+  rewrite Z2Nat.id by (apply Z.mod_pos; lia). rewrite Zplus_mod_idemp_r.
   replace (Z.of_nat base + (Z.of_nat len + Z.of_nat offset - Z.of_nat base))%Z
     with (Z.of_nat len + Z.of_nat offset)%Z by lia.
-  rewrite (Zmod_in_range 1) by lia.
+  rewrite (Z.mod_in_range 1) by lia.
   rewrite Z.mul_1_l, <-Nat2Z.inj_add, <-!Nat2Z.inj_sub,Nat2Z.id; lia.
 Qed.
 
@@ -1361,13 +1441,13 @@ Lemma rotate_nat_sub_add base len offset:
   rotate_nat_sub base (rotate_nat_add base offset len) len = offset.
 Proof.
   intros ?. unfold rotate_nat_add, rotate_nat_sub.
-  rewrite Z2Nat.id by (apply Z_mod_pos; lia).
+  rewrite Z2Nat.id by (apply Z.mod_pos; lia).
   assert (∀ n, (Z.of_nat len + n - Z.of_nat base) = ((Z.of_nat len - Z.of_nat base) + n))%Z
     as -> by naive_solver lia.
   rewrite Zplus_mod_idemp_r.
   replace (Z.of_nat len - Z.of_nat base + (Z.of_nat base + Z.of_nat offset))%Z with
     (Z.of_nat len + Z.of_nat offset)%Z by lia.
-  rewrite (Zmod_in_range 1) by lia.
+  rewrite (Z.mod_in_range 1) by lia.
   rewrite Z.mul_1_l, <-Nat2Z.inj_add, <-!Nat2Z.inj_sub,Nat2Z.id; lia.
 Qed.
 
@@ -1377,7 +1457,7 @@ Lemma rotate_nat_add_add base offset len n:
   (rotate_nat_add base offset len + n) `mod` len.
 Proof.
   intros ?. unfold rotate_nat_add.
-  rewrite !Z2Nat_inj_mod, !Z2Nat.inj_add, !Nat2Z.id by lia.
+  rewrite !Z2Nat.inj_mod, !Z2Nat.inj_add, !Nat2Z.id by lia.
   by rewrite Nat.add_assoc, Nat.add_mod_idemp_l by lia.
 Qed.
 
diff --git a/stdpp/pmap.v b/stdpp/pmap.v
index f269f482cec3454211aa5fec2ad30e7a9d51432a..28acdc293a4647924a732c37dfff3fd08d22ad16 100644
--- a/stdpp/pmap.v
+++ b/stdpp/pmap.v
@@ -85,7 +85,7 @@ Fixpoint Pto_list_raw {A} (j : positive) (t : Pmap_raw A)
     (acc : list (positive * A)) : list (positive * A) :=
   match t with
   | PLeaf => acc
-  | PNode o l r => from_option (λ x, [(Preverse j, x)]) [] o ++
+  | PNode o l r => from_option (λ x, [(Pos.reverse j, x)]) [] o ++
      Pto_list_raw (j~0) l (Pto_list_raw (j~1) r acc)
   end%list.
 Fixpoint Pomap_raw {A B} (f : A → option B) (t : Pmap_raw A) : Pmap_raw B :=
@@ -170,7 +170,7 @@ Lemma Plookup_fmap {A B} (f : A → B) t i : (Pfmap_raw f t) !! i = f <$> t !! i
 Proof. revert i. by induction t; intros [?|?|]; simpl. Qed.
 Lemma Pelem_of_to_list {A} (t : Pmap_raw A) j i acc x :
   (i,x) ∈ Pto_list_raw j t acc ↔
-    (∃ i', i = i' ++ Preverse j ∧ t !! i' = Some x) ∨ (i,x) ∈ acc.
+    (∃ i', i = i' ++ Pos.reverse j ∧ t !! i' = Some x) ∨ (i,x) ∈ acc.
 Proof.
   split.
   { revert j acc. induction t as [|[y|] l IHl r IHr]; intros j acc; simpl.
@@ -178,14 +178,14 @@ Proof.
     - rewrite elem_of_cons. intros [?|?]; simplify_eq.
       { left; exists 1. by rewrite (left_id_L 1 (++))%positive. }
       destruct (IHl (j~0) (Pto_list_raw j~1 r acc)) as [(i'&->&?)|?]; auto.
-      { left; exists (i' ~ 0). by rewrite Preverse_xO, (assoc_L _). }
+      { left; exists (i' ~ 0). by rewrite Pos.reverse_xO, (assoc_L _). }
       destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
-      left; exists (i' ~ 1). by rewrite Preverse_xI, (assoc_L _).
+      left; exists (i' ~ 1). by rewrite Pos.reverse_xI, (assoc_L _).
     - intros.
       destruct (IHl (j~0) (Pto_list_raw j~1 r acc)) as [(i'&->&?)|?]; auto.
-      { left; exists (i' ~ 0). by rewrite Preverse_xO, (assoc_L _). }
+      { left; exists (i' ~ 0). by rewrite Pos.reverse_xO, (assoc_L _). }
       destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
-      left; exists (i' ~ 1). by rewrite Preverse_xI, (assoc_L _). }
+      left; exists (i' ~ 1). by rewrite Pos.reverse_xI, (assoc_L _). }
   revert t j i acc. assert (∀ t j i acc,
     (i, x) ∈ acc → (i, x) ∈ Pto_list_raw j t acc) as help.
   { intros t; induction t as [|[y|] l IHl r IHr]; intros j i acc;
@@ -195,45 +195,45 @@ Proof.
   - done.
   - rewrite elem_of_cons. destruct i as [i|i|]; simplify_eq/=.
     + right. apply help. specialize (IHr (j~1) i).
-      rewrite Preverse_xI, (assoc_L _) in IHr. by apply IHr.
+      rewrite Pos.reverse_xI, (assoc_L _) in IHr. by apply IHr.
     + right. specialize (IHl (j~0) i).
-      rewrite Preverse_xO, (assoc_L _) in IHl. by apply IHl.
+      rewrite Pos.reverse_xO, (assoc_L _) in IHl. by apply IHl.
     + left. by rewrite (left_id_L 1 (++))%positive.
   - destruct i as [i|i|]; simplify_eq/=.
     + apply help. specialize (IHr (j~1) i).
-      rewrite Preverse_xI, (assoc_L _) in IHr. by apply IHr.
+      rewrite Pos.reverse_xI, (assoc_L _) in IHr. by apply IHr.
     + specialize (IHl (j~0) i).
-      rewrite Preverse_xO, (assoc_L _) in IHl. by apply IHl.
+      rewrite Pos.reverse_xO, (assoc_L _) in IHl. by apply IHl.
 Qed.
 Lemma Pto_list_nodup {A} j (t : Pmap_raw A) acc :
-  (∀ i x, (i ++ Preverse j, x) ∈ acc → t !! i = None) →
+  (∀ i x, (i ++ Pos.reverse j, x) ∈ acc → t !! i = None) →
   NoDup acc → NoDup (Pto_list_raw j t acc).
 Proof.
   revert j acc. induction t as [|[y|] l IHl r IHr]; simpl; intros j acc Hin ?.
   - done.
   - repeat constructor.
     { rewrite Pelem_of_to_list. intros [(i&Hi&?)|Hj].
-      { apply (f_equal Plength) in Hi.
-        rewrite Preverse_xO, !Papp_length in Hi; simpl in *; lia. }
+      { apply (f_equal Pos.length) in Hi.
+        rewrite Pos.reverse_xO, !Pos.app_length in Hi; simpl in *; lia. }
       rewrite Pelem_of_to_list in Hj. destruct Hj as [(i&Hi&?)|Hj].
-      { apply (f_equal Plength) in Hi.
-        rewrite Preverse_xI, !Papp_length in Hi; simpl in *; lia. }
+      { apply (f_equal Pos.length) in Hi.
+        rewrite Pos.reverse_xI, !Pos.app_length in Hi; simpl in *; lia. }
       specialize (Hin 1 y). rewrite (left_id_L 1 (++))%positive in Hin.
       discriminate (Hin Hj). }
     apply IHl.
     { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
-      + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
+      + rewrite Pos.reverse_xO, Pos.reverse_xI, !(assoc_L _) in Hi.
         by apply (inj (.++ _)) in Hi.
-      + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
+      + apply (Hin (i~0) x). by rewrite Pos.reverse_xO, (assoc_L _) in Hi. }
     apply IHr; auto. intros i x Hi.
-    apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
+    apply (Hin (i~1) x). by rewrite Pos.reverse_xI, (assoc_L _) in Hi.
   - apply IHl.
     { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
-      + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
+      + rewrite Pos.reverse_xO, Pos.reverse_xI, !(assoc_L _) in Hi.
         by apply (inj (.++ _)) in Hi.
-      + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
+      + apply (Hin (i~0) x). by rewrite Pos.reverse_xO, (assoc_L _) in Hi. }
     apply IHr; auto. intros i x Hi.
-    apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
+    apply (Hin (i~1) x). by rewrite Pos.reverse_xI, (assoc_L _) in Hi.
 Qed.
 Lemma Pomap_lookup {A B} (f : A → option B) t i :
   Pomap_raw f t !! i = t !! i ≫= f.
diff --git a/stdpp/relations.v b/stdpp/relations.v
index c09ae6b9c940961879d4f7a7cee513d3cb9a7a82..5e78f264aae6b1a30e8f1c1139b92df249827d01 100644
--- a/stdpp/relations.v
+++ b/stdpp/relations.v
@@ -150,7 +150,7 @@ Section general.
   Lemma nsteps_r n x y z : nsteps R n x y → R y z → nsteps R (S n) x z.
   Proof. induction 1; eauto. Qed.
 
-  Lemma nsteps_plus_inv n m x z :
+  Lemma nsteps_add_inv n m x z :
     nsteps R (n + m) x z → ∃ y, nsteps R n x y ∧ nsteps R m y z.
   Proof.
     revert x.
@@ -161,7 +161,7 @@ Section general.
   Lemma nsteps_inv_r n x z : nsteps R (S n) x z → ∃ y, nsteps R n x y ∧ R y z.
   Proof.
     rewrite <- PeanoNat.Nat.add_1_r.
-    intros (?&?&?%nsteps_once_inv)%nsteps_plus_inv; eauto.
+    intros (?&?&?%nsteps_once_inv)%nsteps_add_inv; eauto.
   Qed.
 
   Lemma nsteps_congruence {B} (f : A → B) (R' : relation B) n x y :
@@ -171,22 +171,22 @@ Section general.
   (** ** Results about [bsteps] *)
   Lemma bsteps_once n x y : R x y → bsteps R (S n) x y.
   Proof. eauto. Qed.
-  Lemma bsteps_plus_r n m x y :
+  Lemma bsteps_add_r n m x y :
     bsteps R n x y → bsteps R (n + m) x y.
   Proof. induction 1; simpl; eauto. Qed.
   Lemma bsteps_weaken n m x y :
     n ≤ m → bsteps R n x y → bsteps R m x y.
   Proof.
-    intros. rewrite (nat_le_plus_minus n m); auto using bsteps_plus_r.
+    intros. rewrite (Nat.le_add_sub n m); auto using bsteps_add_r.
   Qed.
-  Lemma bsteps_plus_l n m x y :
+  Lemma bsteps_add_l n m x y :
     bsteps R n x y → bsteps R (m + n) x y.
   Proof. apply bsteps_weaken. auto with arith. Qed.
   Lemma bsteps_S n x y :  bsteps R n x y → bsteps R (S n) x y.
   Proof. apply bsteps_weaken. lia. Qed.
   Lemma bsteps_trans n m x y z :
     bsteps R n x y → bsteps R m y z → bsteps R (n + m) x z.
-  Proof. induction 1; simpl; eauto using bsteps_plus_l. Qed.
+  Proof. induction 1; simpl; eauto using bsteps_add_l. Qed.
   Lemma bsteps_r n x y z : bsteps R n x y → R y z → bsteps R (S n) x z.
   Proof. induction 1; eauto. Qed.
   Lemma bsteps_ind_r (P : nat → A → Prop) (x : A)
diff --git a/stdpp/sets.v b/stdpp/sets.v
index 0e6dd8ae399f987088ab7af4c052bbac12889f0f..2e1e3a0687500cab80764a0a7a159cbb22a326e5 100644
--- a/stdpp/sets.v
+++ b/stdpp/sets.v
@@ -1265,17 +1265,17 @@ Section set_seq.
     - rewrite set_seq_subseteq; lia.
   Qed.
 
-  Lemma set_seq_plus_disjoint start len1 len2 :
+  Lemma set_seq_add_disjoint start len1 len2 :
     set_seq (C:=C) start len1 ## set_seq (start + len1) len2.
   Proof. set_solver by lia. Qed.
-  Lemma set_seq_plus start len1 len2 :
+  Lemma set_seq_add start len1 len2 :
     set_seq (C:=C) start (len1 + len2)
     ≡ set_seq start len1 ∪ set_seq (start + len1) len2.
   Proof. set_solver by lia. Qed.
-  Lemma set_seq_plus_L `{!LeibnizEquiv C} start len1 len2 :
+  Lemma set_seq_add_L `{!LeibnizEquiv C} start len1 len2 :
     set_seq (C:=C) start (len1 + len2)
     = set_seq start len1 ∪ set_seq (start + len1) len2.
-  Proof. unfold_leibniz. apply set_seq_plus. Qed.
+  Proof. unfold_leibniz. apply set_seq_add. Qed.
 
   Lemma set_seq_S_start_disjoint start len :
     {[ start ]} ## set_seq (C:=C) (S start) len.
diff --git a/stdpp_unstable/bitblast.v b/stdpp_unstable/bitblast.v
index 04931c2849f1f61f56f389bd9dd6bf9de9aaa197..d82cd2ec7abf6e2bce77cc1f71b221f9825bbe2b 100644
--- a/stdpp_unstable/bitblast.v
+++ b/stdpp_unstable/bitblast.v
@@ -247,7 +247,7 @@ Lemma bitblast_id_bounded z z' n :
   Bitblast z n (bool_decide (0 ≤ n < z') && BITBLAST_TESTBIT z n).
 Proof.
   move => [Hb]. constructor.
-  move: (Hb) => /Z_bounded_iff_bits_nonneg' Hn.
+  move: (Hb) => /Z.bounded_iff_bits_nonneg' Hn.
   case_bool_decide => //=.
   destruct (decide (0 ≤ n)); [|rewrite Z.testbit_neg_r //; lia].
   apply Hn; try lia.
@@ -384,7 +384,7 @@ Proof.
   move => [->] [<-]. constructor.
   case_bool_decide => /=. { rewrite Z.pow_neg_r ?bool_decide_false /= ?orb_false_r; [done|lia..]. }
   destruct (decide (0 ≤ n)). 2: { rewrite !Z.testbit_neg_r ?andb_false_r //; lia. }
-  rewrite -Z.land_ones; [|lia]. rewrite Z.land_spec Z_ones_spec; [|lia..].
+  rewrite -Z.land_ones; [|lia]. rewrite Z.land_spec Z.ones_spec; [|lia..].
   by rewrite andb_comm.
 Qed.
 Global Hint Resolve bitblast_mod | 10 : bitblast.
diff --git a/tests/bitblast.v b/tests/bitblast.v
index 540082beaed716825e8b64297ad1666ffce86c90..e68bbfc8b5a4c4149e18f735a57eb107e9f7fe41 100644
--- a/tests/bitblast.v
+++ b/tests/bitblast.v
@@ -32,7 +32,7 @@ Goal ∀ z, 0 ≤ z < 2 ^ 64 →
 Proof.
   intros z ?. split.
   - intros Hx. split.
-    + apply Z_bounded_iff_bits_nonneg; [lia..|]. intros n ?. bitblast.
+    + apply Z.bounded_iff_bits_nonneg; [lia..|]. intros n ?. bitblast.
       by bitblast Hx with n.
     + bitblast as n. by bitblast Hx with n.
   - intros [H1 H2]. bitblast as n. by bitblast H2 with n.