diff --git a/CHANGELOG.md b/CHANGELOG.md
index c8b9617a33ab01205b0e8a62bed6ca3ad550591f..f10c6edfdddacfcdcbdc445d776db40af233ba05 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -53,6 +53,9 @@ With this release, we dropped support for Coq 8.9.
   equal to `✓ b`.
 * Add `mnat_auth`, a wrapper for `auth max_nat`. The result is an authoritative
   `nat` where a fragment is a lower bound whose ownership is persistent.
+* Change `*_valid` lemma statements involving fractions to use `Qp` addition and
+  inequality instead of RA composition and validity (also in `base_logic` and
+  the higher layers).
 
 **Changes in `bi`:**
 
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 4baed6ce497e549ac994305c77cb8cc05d713ae2..6adb6c2e4f2ffe3e363b2fa599f1b55270035c39 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -154,13 +154,13 @@ Section auth.
     ✓ (●{p} a ⋅ ●{q} b) → a = b.
   Proof. by apply view_auth_frac_op_inv_L. Qed.
 
-  Lemma auth_auth_frac_validN n q a : ✓{n} (●{q} a) ↔ ✓{n} q ∧ ✓{n} a.
+  Lemma auth_auth_frac_validN n q a : ✓{n} (●{q} a) ↔ (q ≤ 1)%Qp ∧ ✓{n} a.
   Proof. by rewrite view_auth_frac_validN auth_view_rel_unit. Qed.
   Lemma auth_auth_validN n a : ✓{n} (● a) ↔ ✓{n} a.
   Proof. by rewrite view_auth_validN auth_view_rel_unit. Qed.
 
   Lemma auth_auth_frac_op_validN n q1 q2 a1 a2 :
-    ✓{n} (●{q1} a1 ⋅ ●{q2} a2) ↔ ✓ (q1 + q2)%Qp ∧ a1 ≡{n}≡ a2 ∧ ✓{n} a1.
+    ✓{n} (●{q1} a1 ⋅ ●{q2} a2) ↔ (q1 + q2 ≤ 1)%Qp ∧ a1 ≡{n}≡ a2 ∧ ✓{n} a1.
   Proof. by rewrite view_auth_frac_op_validN auth_view_rel_unit. Qed.
   Lemma auth_auth_op_validN n a1 a2 : ✓{n} (● a1 ⋅ ● a2) ↔ False.
   Proof. apply view_auth_op_validN. Qed.
@@ -181,12 +181,12 @@ Section auth.
   Proof. apply auth_frag_op_validN. Qed.
 
   Lemma auth_both_frac_validN n q a b :
-    ✓{n} (●{q} a ⋅ ◯ b) ↔ ✓{n} q ∧ b ≼{n} a ∧ ✓{n} a.
+    ✓{n} (●{q} a ⋅ ◯ b) ↔ (q ≤ 1)%Qp ∧ b ≼{n} a ∧ ✓{n} a.
   Proof. apply view_both_frac_validN. Qed.
   Lemma auth_both_validN n a b : ✓{n} (● a ⋅ ◯ b) ↔ b ≼{n} a ∧ ✓{n} a.
   Proof. apply view_both_validN. Qed.
 
-  Lemma auth_auth_frac_valid q a : ✓ (●{q} a) ↔ ✓ q ∧ ✓ a.
+  Lemma auth_auth_frac_valid q a : ✓ (●{q} a) ↔ (q ≤ 1)%Qp ∧ ✓ a.
   Proof.
     rewrite view_auth_frac_valid !cmra_valid_validN.
     by setoid_rewrite auth_view_rel_unit.
@@ -198,10 +198,10 @@ Section auth.
   Qed.
 
   Lemma auth_auth_frac_op_valid q1 q2 a1 a2 :
-    ✓ (●{q1} a1 ⋅ ●{q2} a2) ↔ ✓ (q1 + q2)%Qp ∧ a1 ≡ a2 ∧ ✓ a1.
+    ✓ (●{q1} a1 ⋅ ●{q2} a2) ↔ (q1 + q2 ≤ 1)%Qp ∧ a1 ≡ a2 ∧ ✓ a1.
   Proof.
     rewrite view_auth_frac_op_valid !cmra_valid_validN.
-    by setoid_rewrite auth_view_rel_unit.
+    setoid_rewrite auth_view_rel_unit. done.
   Qed.
   Lemma auth_auth_op_valid a1 a2 : ✓ (● a1 ⋅ ● a2) ↔ False.
   Proof. apply view_auth_op_valid. Qed.
@@ -228,7 +228,7 @@ Section auth.
   single witness for [b ≼ a] from validity, we have to make do with one witness
   per step-index, i.e., [∀ n, b ≼{n} a]. *)
   Lemma auth_both_frac_valid q a b :
-    ✓ (●{q} a ⋅ ◯ b) ↔ ✓ q ∧ (∀ n, b ≼{n} a) ∧ ✓ a.
+    ✓ (●{q} a ⋅ ◯ b) ↔ (q ≤ 1)%Qp ∧ (∀ n, b ≼{n} a) ∧ ✓ a.
   Proof.
     rewrite view_both_frac_valid. apply and_iff_compat_l. split.
     - intros Hrel. split.
@@ -238,11 +238,11 @@ Section auth.
   Qed.
   Lemma auth_both_valid a b :
     ✓ (● a ⋅ ◯ b) ↔ (∀ n, b ≼{n} a) ∧ ✓ a.
-  Proof. rewrite auth_both_frac_valid frac_valid'. naive_solver. Qed.
+  Proof. rewrite auth_both_frac_valid. naive_solver. Qed.
 
   (* The reverse direction of the two lemmas below only holds if the camera is
   discrete. *)
-  Lemma auth_both_frac_valid_2 q a b : ✓ q → ✓ a → b ≼ a → ✓ (●{q} a ⋅ ◯ b).
+  Lemma auth_both_frac_valid_2 q a b : (q ≤ 1)%Qp → ✓ a → b ≼ a → ✓ (●{q} a ⋅ ◯ b).
   Proof.
     intros. apply auth_both_frac_valid.
     naive_solver eauto using cmra_included_includedN.
@@ -251,14 +251,14 @@ Section auth.
   Proof. intros ??. by apply auth_both_frac_valid_2. Qed.
 
   Lemma auth_both_frac_valid_discrete `{!CmraDiscrete A} q a b :
-    ✓ (●{q} a ⋅ ◯ b) ↔ ✓ q ∧ b ≼ a ∧ ✓ a.
+    ✓ (●{q} a ⋅ ◯ b) ↔ (q ≤ 1)%Qp ∧ b ≼ a ∧ ✓ a.
   Proof.
     rewrite auth_both_frac_valid. setoid_rewrite <-cmra_discrete_included_iff.
     naive_solver eauto using O.
   Qed.
   Lemma auth_both_valid_discrete `{!CmraDiscrete A} a b :
     ✓ (● a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
-  Proof. rewrite auth_both_frac_valid_discrete frac_valid'. naive_solver. Qed.
+  Proof. rewrite auth_both_frac_valid_discrete. naive_solver. Qed.
 
   (** Inclusion *)
   Lemma auth_auth_frac_includedN n p1 p2 a1 a2 b :
diff --git a/theories/algebra/lib/frac_agree.v b/theories/algebra/lib/frac_agree.v
index d2e805d776cede6ee63061770c508771e4d72848..af00e2bf85269b4e0ec6618aa2c8106e11a46723 100644
--- a/theories/algebra/lib/frac_agree.v
+++ b/theories/algebra/lib/frac_agree.v
@@ -31,18 +31,18 @@ Section lemmas.
 
   Lemma frac_agree_op_valid q1 a1 q2 a2 :
     ✓ (to_frac_agree q1 a1 ⋅ to_frac_agree q2 a2) →
-    ✓ (q1 + q2)%Qp ∧ a1 ≡ a2.
+    (q1 + q2 ≤ 1)%Qp ∧ a1 ≡ a2.
   Proof.
     intros [Hq Ha]%pair_valid. simpl in *. split; first done.
     apply to_agree_op_inv. done.
   Qed.
   Lemma frac_agree_op_valid_L `{!LeibnizEquiv A} q1 a1 q2 a2 :
     ✓ (to_frac_agree q1 a1 ⋅ to_frac_agree q2 a2) →
-    ✓ (q1 + q2)%Qp ∧ a1 = a2.
+    (q1 + q2 ≤ 1)%Qp ∧ a1 = a2.
   Proof. unfold_leibniz. apply frac_agree_op_valid. Qed.
   Lemma frac_agree_op_validN q1 a1 q2 a2 n :
     ✓{n} (to_frac_agree q1 a1 ⋅ to_frac_agree q2 a2) →
-    ✓ (q1 + q2)%Qp ∧ a1 ≡{n}≡ a2.
+    (q1 + q2 ≤ 1)%Qp ∧ a1 ≡{n}≡ a2.
   Proof.
     intros [Hq Ha]%pair_validN. simpl in *. split; first done.
     apply to_agree_op_invN. done.
diff --git a/theories/algebra/lib/frac_auth.v b/theories/algebra/lib/frac_auth.v
index 8624b79a53e2e49e3ae6d2dac35143c13d5faeb6..d9a1f62fb929b9001b430edaecda2019194c8d21 100644
--- a/theories/algebra/lib/frac_auth.v
+++ b/theories/algebra/lib/frac_auth.v
@@ -83,18 +83,18 @@ Section frac_auth.
   Lemma frac_auth_auth_valid a : ✓ (●F a) ↔ ✓ a.
   Proof. rewrite !cmra_valid_validN. by setoid_rewrite frac_auth_auth_validN. Qed.
 
-  Lemma frac_auth_frag_validN n q a : ✓{n} (◯F{q} a) ↔ ✓{n} q ∧ ✓{n} a.
+  Lemma frac_auth_frag_validN n q a : ✓{n} (◯F{q} a) ↔ (q ≤ 1)%Qp ∧ ✓{n} a.
   Proof. by rewrite /frac_auth_frag auth_frag_validN. Qed.
-  Lemma frac_auth_frag_valid q a : ✓ (◯F{q} a) ↔ ✓ q ∧ ✓ a.
+  Lemma frac_auth_frag_valid q a : ✓ (◯F{q} a) ↔ (q ≤ 1)%Qp ∧ ✓ a.
   Proof. by rewrite /frac_auth_frag auth_frag_valid. Qed.
 
   Lemma frac_auth_frag_op q1 q2 a1 a2 : ◯F{q1+q2} (a1 ⋅ a2) ≡ ◯F{q1} a1 ⋅ ◯F{q2} a2.
   Proof. done. Qed.
 
   Lemma frac_auth_frag_validN_op_1_l n q a b : ✓{n} (◯F{1} a ⋅ ◯F{q} b) → False.
-  Proof. rewrite -frac_auth_frag_op frac_auth_frag_validN=> -[/exclusiveN_l []]. Qed.
+  Proof. rewrite -frac_auth_frag_op frac_auth_frag_validN=> -[/Qp_not_add_le_l []]. Qed.
   Lemma frac_auth_frag_valid_op_1_l q a b : ✓ (◯F{1} a ⋅ ◯F{q} b) → False.
-  Proof. rewrite -frac_auth_frag_op frac_auth_frag_valid=> -[/exclusive_l []]. Qed.
+  Proof. rewrite -frac_auth_frag_op frac_auth_frag_valid=> -[/Qp_not_add_le_l []]. Qed.
 
   Global Instance frac_auth_is_op (q q1 q2 : frac) (a a1 a2 : A) :
     IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2).
diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v
index 5439678fe2d96668698cff38de46f8ccdaa23367..5e7806135e12740c510fb8c4830c305fd18653c3 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/theories/algebra/lib/gmap_view.v
@@ -194,7 +194,7 @@ Section lemmas.
     ✓ (gmap_view_auth p m1 ⋅ gmap_view_auth q m2) → m1 = m2.
   Proof. apply view_auth_frac_op_inv_L, _. Qed.
 
-  Lemma gmap_view_auth_frac_valid m q : ✓ gmap_view_auth q m ↔ ✓ q.
+  Lemma gmap_view_auth_frac_valid m q : ✓ gmap_view_auth q m ↔ (q ≤ 1)%Qp.
   Proof.
     rewrite view_auth_frac_valid. intuition eauto using gmap_view_rel_unit.
   Qed.
@@ -202,7 +202,7 @@ Section lemmas.
   Proof. rewrite gmap_view_auth_frac_valid. done. Qed.
 
   Lemma gmap_view_auth_frac_op_valid q1 q2 m1 m2 :
-    ✓ (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2) ↔ ✓ (q1 + q2)%Qp ∧ m1 ≡ m2.
+    ✓ (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2) ↔ (q1 + q2 ≤ 1)%Qp ∧ m1 ≡ m2.
   Proof.
     rewrite view_auth_frac_op_valid. intuition eauto using gmap_view_rel_unit.
   Qed.
@@ -251,7 +251,7 @@ Section lemmas.
 
   Lemma gmap_view_both_frac_validN n q m k dq v :
     ✓{n} (gmap_view_auth q m ⋅ gmap_view_frag k dq v) ↔
-      ✓ q ∧ ✓ dq ∧ m !! k ≡{n}≡ Some v.
+      (q ≤ 1)%Qp ∧ ✓ dq ∧ m !! k ≡{n}≡ Some v.
   Proof.
     rewrite /gmap_view_auth /gmap_view_frag.
     rewrite view_both_frac_validN gmap_view_rel_lookup.
@@ -263,7 +263,7 @@ Section lemmas.
   Proof. rewrite gmap_view_both_frac_validN. naive_solver done. Qed.
   Lemma gmap_view_both_frac_valid q m k dq v :
     ✓ (gmap_view_auth q m ⋅ gmap_view_frag k dq v) ↔
-    ✓ q ∧ ✓ dq ∧ m !! k ≡ Some v.
+    (q ≤ 1)%Qp ∧ ✓ dq ∧ m !! k ≡ Some v.
   Proof.
     rewrite /gmap_view_auth /gmap_view_frag.
     rewrite view_both_frac_valid. setoid_rewrite gmap_view_rel_lookup.
diff --git a/theories/algebra/lib/mnat_auth.v b/theories/algebra/lib/mnat_auth.v
index fe5b64dda8ef2926bd11d97b3c0e586449462c58..aa3c062eb587d2dfd9da9c7c2c68aed0102a6273 100644
--- a/theories/algebra/lib/mnat_auth.v
+++ b/theories/algebra/lib/mnat_auth.v
@@ -43,7 +43,7 @@ Section mnat_auth.
   Proof. intros. rewrite mnat_auth_frag_op Nat.max_r //. Qed.
 
   Lemma mnat_auth_frac_op_valid q1 q2 n1 n2 :
-    ✓ (mnat_auth_auth q1 n1 ⋅ mnat_auth_auth q2 n2) ↔ ✓ (q1 + q2)%Qp ∧ n1 = n2.
+    ✓ (mnat_auth_auth q1 n1 ⋅ mnat_auth_auth q2 n2) ↔ (q1 + q2 ≤ 1)%Qp ∧ n1 = n2.
   Proof.
     rewrite /mnat_auth_auth (comm _ (●{q2} _)) -!assoc (assoc _ (◯ _)).
     rewrite -auth_frag_op (comm _ (â—¯ _)) assoc. split.
@@ -57,7 +57,7 @@ Section mnat_auth.
   Proof. rewrite mnat_auth_frac_op_valid. naive_solver. Qed.
 
   Lemma mnat_auth_both_frac_valid q n m :
-    ✓ (mnat_auth_auth q n ⋅ mnat_auth_frag m) ↔ ✓ q ∧ m ≤ n.
+    ✓ (mnat_auth_auth q n ⋅ mnat_auth_frag m) ↔ (q ≤ 1)%Qp ∧ m ≤ n.
   Proof.
     rewrite /mnat_auth_auth /mnat_auth_frag -assoc -auth_frag_op.
     rewrite auth_both_frac_valid_discrete max_nat_included /=.
@@ -66,7 +66,7 @@ Section mnat_auth.
 
   Lemma mnat_auth_both_valid n m :
     ✓ (mnat_auth_auth 1 n ⋅ mnat_auth_frag m) ↔ m ≤ n.
-  Proof. rewrite mnat_auth_both_frac_valid frac_valid'. naive_solver. Qed.
+  Proof. rewrite mnat_auth_both_frac_valid. naive_solver. Qed.
 
   Lemma mnat_auth_frag_mono n1 n2 : n1 ≤ n2 → mnat_auth_frag n1 ≼ mnat_auth_frag n2.
   Proof. intros. by apply auth_frag_mono, max_nat_included. Qed.
diff --git a/theories/algebra/lib/ufrac_auth.v b/theories/algebra/lib/ufrac_auth.v
index f6bc39b74e50c45024599b61f84f500f487ee771..e2ab06b4e8595e9cfc40b93629b561b294358b10 100644
--- a/theories/algebra/lib/ufrac_auth.v
+++ b/theories/algebra/lib/ufrac_auth.v
@@ -29,7 +29,7 @@ Definition ufrac_authUR (A : cmraT) : ucmraT :=
 [q : Qp] instead of [q : ufrac]. This way, the API does not expose that [ufrac]
 is used internally. This is quite important, as there are two canonical camera
 instances with carrier [Qp], namely [fracR] and [ufracR]. When writing things
-like [ufrac_auth_auth q a ∧ ✓{q}] we want Coq to infer the type of [q] as [Qp]
+like [ufrac_auth_auth q a ∧ ✓ q] we want Coq to infer the type of [q] as [Qp]
 such that the [✓] of the default [fracR] camera is used, and not the [✓] of
 the [ufracR] camera. *)
 Definition ufrac_auth_auth {A : cmraT} (q : Qp) (x : A) : ufrac_authR A :=
diff --git a/theories/algebra/view.v b/theories/algebra/view.v
index a13cb3511a5f094790be4c3872c74aba498f047b..e8ad6e623f9ed8489e1a08fb29721a8413f4eae5 100644
--- a/theories/algebra/view.v
+++ b/theories/algebra/view.v
@@ -317,18 +317,16 @@ Section cmra.
     ✓ (●V{p1} a1 ⋅ ●V{p2} a2) → a1 = a2.
   Proof. by intros ?%view_auth_frac_op_inv%leibniz_equiv. Qed.
 
-  Lemma view_auth_frac_validN n q a : ✓{n} (●V{q} a) ↔ ✓{n} q ∧ rel n a ε.
+  Lemma view_auth_frac_validN n q a : ✓{n} (●V{q} a) ↔ (q ≤ 1)%Qp ∧ rel n a ε.
   Proof.
     rewrite view_validN_eq /=. apply and_iff_compat_l. split; [|by eauto].
     by intros [? [->%(inj to_agree) ?]].
   Qed.
   Lemma view_auth_validN n a : ✓{n} (●V a) ↔ rel n a ε.
-  Proof.
-    rewrite view_auth_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
-  Qed.
+  Proof. rewrite view_auth_frac_validN. naive_solver. Qed.
 
   Lemma view_auth_frac_op_validN n q1 q2 a1 a2 :
-    ✓{n} (●V{q1} a1 ⋅ ●V{q2} a2) ↔ ✓ (q1 + q2)%Qp ∧ a1 ≡{n}≡ a2 ∧ rel n a1 ε.
+    ✓{n} (●V{q1} a1 ⋅ ●V{q2} a2) ↔ (q1 + q2 ≤ 1)%Qp ∧ a1 ≡{n}≡ a2 ∧ rel n a1 ε.
   Proof.
     split.
     - intros Hval. assert (a1 ≡{n}≡ a2) as Ha by eauto using view_auth_frac_op_invN.
@@ -342,30 +340,29 @@ Section cmra.
   Proof. done. Qed.
 
   Lemma view_both_frac_validN n q a b :
-    ✓{n} (●V{q} a ⋅ ◯V b) ↔ ✓{n} q ∧ rel n a b.
+    ✓{n} (●V{q} a ⋅ ◯V b) ↔ (q ≤ 1)%Qp ∧ rel n a b.
   Proof.
     rewrite view_validN_eq /=. apply and_iff_compat_l.
     setoid_rewrite (left_id _ _ b). split; [|by eauto].
     by intros [?[->%(inj to_agree)]].
   Qed.
   Lemma view_both_validN n a b : ✓{n} (●V a ⋅ ◯V b) ↔ rel n a b.
-  Proof.
-    rewrite view_both_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
-  Qed.
+  Proof. rewrite view_both_frac_validN. naive_solver. Qed.
 
-  Lemma view_auth_frac_valid q a : ✓ (●V{q} a) ↔ ✓ q ∧ ∀ n, rel n a ε.
+  Lemma view_auth_frac_valid q a : ✓ (●V{q} a) ↔ (q ≤ 1)%Qp ∧ ∀ n, rel n a ε.
   Proof.
     rewrite view_valid_eq /=. apply and_iff_compat_l. split; [|by eauto].
     intros H n. by destruct (H n) as [? [->%(inj to_agree) ?]].
   Qed.
   Lemma view_auth_valid a : ✓ (●V a) ↔ ∀ n, rel n a ε.
-  Proof. rewrite view_auth_frac_valid frac_valid'. naive_solver. Qed.
+  Proof. rewrite view_auth_frac_valid. naive_solver. Qed.
 
   Lemma view_auth_frac_op_valid q1 q2 a1 a2 :
-    ✓ (●V{q1} a1 ⋅ ●V{q2} a2) ↔ ✓ (q1 + q2)%Qp ∧ a1 ≡ a2 ∧ ∀ n, rel n a1 ε.
+    ✓ (●V{q1} a1 ⋅ ●V{q2} a2) ↔ (q1 + q2 ≤ 1)%Qp ∧ a1 ≡ a2 ∧ ∀ n, rel n a1 ε.
   Proof.
     rewrite !cmra_valid_validN equiv_dist. setoid_rewrite view_auth_frac_op_validN.
-    setoid_rewrite <-cmra_discrete_valid_iff. naive_solver.
+    split; last naive_solver. intros Hv.
+    split; last naive_solver. apply (Hv 0).
   Qed.
   Lemma view_auth_op_valid a1 a2 : ✓ (●V a1 ⋅ ●V a2) ↔ False.
   Proof. rewrite view_auth_frac_op_valid. naive_solver. Qed.
@@ -373,14 +370,14 @@ Section cmra.
   Lemma view_frag_valid b : ✓ (◯V b) ↔ ∀ n, ∃ a, rel n a b.
   Proof. done. Qed.
 
-  Lemma view_both_frac_valid q a b : ✓ (●V{q} a ⋅ ◯V b) ↔ ✓ q ∧ ∀ n, rel n a b.
+  Lemma view_both_frac_valid q a b : ✓ (●V{q} a ⋅ ◯V b) ↔ (q ≤ 1)%Qp ∧ ∀ n, rel n a b.
   Proof.
     rewrite view_valid_eq /=. apply and_iff_compat_l.
     setoid_rewrite (left_id _ _ b). split; [|by eauto].
     intros H n. by destruct (H n) as [?[->%(inj to_agree)]].
   Qed.
   Lemma view_both_valid a b : ✓ (●V a ⋅ ◯V b) ↔ ∀ n, rel n a b.
-  Proof. rewrite view_both_frac_valid frac_valid'. naive_solver. Qed.
+  Proof. rewrite view_both_frac_valid. naive_solver. Qed.
 
   (** Inclusion *)
   Lemma view_auth_frac_includedN n p1 p2 a1 a2 b :
diff --git a/theories/base_logic/algebra.v b/theories/base_logic/algebra.v
index e6dc7794dba298bca8badb95b6afc9dc962ef2f5..51a5c1673f50d325f940cd7836ed2cc70624746b 100644
--- a/theories/base_logic/algebra.v
+++ b/theories/base_logic/algebra.v
@@ -8,21 +8,28 @@ From iris Require Import options.
 Section upred.
 Context {M : ucmraT}.
 
-Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢@{uPredI M} ✓ x.1 ∧ ✓ x.2.
+(* Force implicit argument M *)
+Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
+Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
+
+Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
 Proof. by uPred.unseal. Qed.
 Lemma option_validI {A : cmraT} (mx : option A) :
-  ✓ mx ⊣⊢@{uPredI M} match mx with Some x => ✓ x | None => True : uPred M end.
+  ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
 Proof. uPred.unseal. by destruct mx. Qed.
 Lemma discrete_fun_validI {A} {B : A → ucmraT} (g : discrete_fun B) :
-  ✓ g ⊣⊢@{uPredI M} ∀ i, ✓ g i.
+  ✓ g ⊣⊢ ∀ i, ✓ g i.
 Proof. by uPred.unseal. Qed.
 
+Lemma frac_validI (q : Qp) : ✓ q ⊣⊢ ⌜q ≤ 1⌝%Qp.
+Proof. rewrite uPred.discrete_valid frac_valid' //. Qed.
+
 Section gmap_ofe.
   Context `{Countable K} {A : ofeT}.
   Implicit Types m : gmap K A.
   Implicit Types i : K.
 
-  Lemma gmap_equivI m1 m2 : m1 ≡ m2 ⊣⊢@{uPredI M} ∀ i, m1 !! i ≡ m2 !! i.
+  Lemma gmap_equivI m1 m2 : m1 ≡ m2 ⊣⊢ ∀ i, m1 !! i ≡ m2 !! i.
   Proof. by uPred.unseal. Qed.
 End gmap_ofe.
 
@@ -30,9 +37,9 @@ Section gmap_cmra.
   Context `{Countable K} {A : cmraT}.
   Implicit Types m : gmap K A.
 
-  Lemma gmap_validI m : ✓ m ⊣⊢@{uPredI M} ∀ i, ✓ (m !! i).
+  Lemma gmap_validI m : ✓ m ⊣⊢ ∀ i, ✓ (m !! i).
   Proof. by uPred.unseal. Qed.
-  Lemma singleton_validI i x : ✓ ({[ i := x ]} : gmap K A) ⊣⊢@{uPredI M} ✓ x.
+  Lemma singleton_validI i x : ✓ ({[ i := x ]} : gmap K A) ⊣⊢ ✓ x.
   Proof.
     rewrite gmap_validI. apply: anti_symm.
     - rewrite (bi.forall_elim i) lookup_singleton option_validI. done.
@@ -47,7 +54,7 @@ Section list_ofe.
   Context {A : ofeT}.
   Implicit Types l : list A.
 
-  Lemma list_equivI l1 l2 : l1 ≡ l2 ⊣⊢@{uPredI M} ∀ i, l1 !! i ≡ l2 !! i.
+  Lemma list_equivI l1 l2 : l1 ≡ l2 ⊣⊢ ∀ i, l1 !! i ≡ l2 !! i.
   Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
 End list_ofe.
 
@@ -55,7 +62,7 @@ Section list_cmra.
   Context {A : ucmraT}.
   Implicit Types l : list A.
 
-  Lemma list_validI l : ✓ l ⊣⊢@{uPredI M} ∀ i, ✓ (l !! i).
+  Lemma list_validI l : ✓ l ⊣⊢ ∀ i, ✓ (l !! i).
   Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed.
 End list_cmra.
 
@@ -65,7 +72,7 @@ Section excl.
   Implicit Types x y : excl A.
 
   Lemma excl_equivI x y :
-    x ≡ y ⊣⊢@{uPredI M} match x, y with
+    x ≡ y ⊣⊢ match x, y with
                         | Excl a, Excl b => a ≡ b
                         | ExclBot, ExclBot => True
                         | _, _ => False
@@ -74,7 +81,7 @@ Section excl.
     uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
   Qed.
   Lemma excl_validI x :
-    ✓ x ⊣⊢@{uPredI M} if x is ExclBot then False else True.
+    ✓ x ⊣⊢ if x is ExclBot then False else True.
   Proof. uPred.unseal. by destruct x. Qed.
 End excl.
 
@@ -83,16 +90,16 @@ Section agree.
   Implicit Types a b : A.
   Implicit Types x y : agree A.
 
-  Lemma agree_equivI a b : to_agree a ≡ to_agree b ⊣⊢@{uPredI M} (a ≡ b).
+  Lemma agree_equivI a b : to_agree a ≡ to_agree b ⊣⊢ (a ≡ b).
   Proof.
     uPred.unseal. do 2 split.
     - intros Hx. exact: (inj to_agree).
     - intros Hx. exact: to_agree_ne.
   Qed.
-  Lemma agree_validI x y : ✓ (x ⋅ y) ⊢@{uPredI M} x ≡ y.
+  Lemma agree_validI x y : ✓ (x ⋅ y) ⊢ x ≡ y.
   Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed.
 
-  Lemma to_agree_uninjI x : ✓ x ⊢@{uPredI M} ∃ a, to_agree a ≡ x.
+  Lemma to_agree_uninjI x : ✓ x ⊢ ∃ a, to_agree a ≡ x.
   Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
 End agree.
 
@@ -102,7 +109,7 @@ Section csum_ofe.
   Implicit Types b : B.
 
   Lemma csum_equivI (x y : csum A B) :
-    x ≡ y ⊣⊢@{uPredI M} match x, y with
+    x ≡ y ⊣⊢ match x, y with
                         | Cinl a, Cinl a' => a ≡ a'
                         | Cinr b, Cinr b' => b ≡ b'
                         | CsumBot, CsumBot => True
@@ -120,7 +127,7 @@ Section csum_cmra.
   Implicit Types b : B.
 
   Lemma csum_validI (x : csum A B) :
-    ✓ x ⊣⊢@{uPredI M} match x with
+    ✓ x ⊣⊢ match x with
                       | Cinl a => ✓ a
                       | Cinr b => ✓ b
                       | CsumBot => False
@@ -137,21 +144,21 @@ Section view.
 
   Lemma view_both_frac_validI_1 (relI : uPred M) q a b :
     (∀ n (x : M), rel n a b → relI n x) →
-    ✓ (●V{q} a ⋅ ◯V b : view rel) ⊢ ✓ q ∧ relI.
+    ✓ (●V{q} a ⋅ ◯V b : view rel) ⊢ ⌜q ≤ 1⌝%Qp ∧ relI.
   Proof.
     intros Hrel. uPred.unseal. split=> n x _ /=.
     rewrite /uPred_holds /= view_both_frac_validN. by move=> [? /Hrel].
   Qed.
   Lemma view_both_frac_validI_2 (relI : uPred M) q a b :
     (∀ n (x : M), relI n x → rel n a b) →
-    ✓ q ∧ relI ⊢ ✓ (●V{q} a ⋅ ◯V b : view rel).
+    ⌜q ≤ 1⌝%Qp ∧ relI ⊢ ✓ (●V{q} a ⋅ ◯V b : view rel).
   Proof.
     intros Hrel. uPred.unseal. split=> n x _ /=.
     rewrite /uPred_holds /= view_both_frac_validN. by move=> [? /Hrel].
   Qed.
   Lemma view_both_frac_validI (relI : uPred M) q a b :
     (∀ n (x : M), rel n a b ↔ relI n x) →
-    ✓ (●V{q} a ⋅ ◯V b : view rel) ⊣⊢ ✓ q ∧ relI.
+    ✓ (●V{q} a ⋅ ◯V b : view rel) ⊣⊢ ⌜q ≤ 1⌝%Qp ∧ relI.
   Proof.
     intros. apply (anti_symm _);
       [apply view_both_frac_validI_1|apply view_both_frac_validI_2]; naive_solver.
@@ -165,7 +172,7 @@ Section view.
     (∀ n (x : M), relI n x → rel n a b) →
     relI ⊢ ✓ (●V a ⋅ ◯V b : view rel).
   Proof.
-    intros. rewrite -view_both_frac_validI_2 // uPred.discrete_valid.
+    intros. rewrite -view_both_frac_validI_2 //.
     apply bi.and_intro; [|done]. by apply bi.pure_intro.
   Qed.
   Lemma view_both_validI (relI : uPred M) a b :
@@ -178,7 +185,7 @@ Section view.
 
   Lemma view_auth_frac_validI (relI : uPred M) q a :
     (∀ n (x : M), relI n x ↔ rel n a ε) →
-    ✓ (●V{q} a : view rel) ⊣⊢ ✓ q ∧ relI.
+    ✓ (●V{q} a : view rel) ⊣⊢ ⌜q ≤ 1⌝%Qp ∧ relI.
   Proof.
     intros. rewrite -(right_id ε op (●V{q} a)). by apply view_both_frac_validI.
   Qed.
@@ -189,7 +196,7 @@ Section view.
 
   Lemma view_frag_validI (relI : uPred M) b :
     (∀ n (x : M), relI n x ↔ ∃ a, rel n a b) →
-    ✓ (◯V b : view rel) ⊣⊢@{uPredI M} relI.
+    ✓ (◯V b : view rel) ⊣⊢ relI.
   Proof. uPred.unseal=> Hrel. split=> n x _. by rewrite Hrel. Qed.
 End view.
 
@@ -198,29 +205,29 @@ Section auth.
   Implicit Types a b : A.
   Implicit Types x y : auth A.
 
-  Lemma auth_auth_frac_validI q a : ✓ (●{q} a) ⊣⊢@{uPredI M} ✓ q ∧ ✓ a.
+  Lemma auth_auth_frac_validI q a : ✓ (●{q} a) ⊣⊢ ⌜q ≤ 1⌝%Qp ∧ ✓ a.
   Proof.
     apply view_auth_frac_validI=> n. uPred.unseal; split; [|by intros [??]].
     split; [|done]. apply ucmra_unit_leastN.
   Qed.
-  Lemma auth_auth_validI a : ✓ (● a) ⊣⊢@{uPredI M} ✓ a.
+  Lemma auth_auth_validI a : ✓ (● a) ⊣⊢ ✓ a.
   Proof.
-    by rewrite auth_auth_frac_validI uPred.discrete_valid bi.pure_True // left_id.
+    by rewrite auth_auth_frac_validI bi.pure_True // left_id.
   Qed.
 
-  Lemma auth_frag_validI a : ✓ (◯ a) ⊣⊢@{uPredI M} ✓ a.
+  Lemma auth_frag_validI a : ✓ (◯ a) ⊣⊢ ✓ a.
   Proof.
     apply view_frag_validI=> n x.
     rewrite auth_view_rel_exists. by uPred.unseal.
   Qed.
 
   Lemma auth_both_frac_validI q a b :
-    ✓ (●{q} a ⋅ ◯ b) ⊣⊢@{uPredI M} ✓ q ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
+    ✓ (●{q} a ⋅ ◯ b) ⊣⊢ ⌜q ≤ 1⌝%Qp ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
   Proof. apply view_both_frac_validI=> n. by uPred.unseal. Qed.
   Lemma auth_both_validI a b :
-    ✓ (● a ⋅ ◯ b) ⊣⊢@{uPredI M} (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
+    ✓ (● a ⋅ ◯ b) ⊣⊢ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
   Proof.
-    by rewrite auth_both_frac_validI uPred.discrete_valid bi.pure_True // left_id.
+    by rewrite auth_both_frac_validI bi.pure_True // left_id.
   Qed.
 
 End auth.
@@ -229,7 +236,7 @@ Section excl_auth.
   Context {A : ofeT}.
   Implicit Types a b : A.
 
-  Lemma excl_auth_agreeI a b : ✓ (●E a ⋅ ◯E b) ⊢@{uPredI M} (a ≡ b).
+  Lemma excl_auth_agreeI a b : ✓ (●E a ⋅ ◯E b) ⊢ (a ≡ b).
   Proof.
     rewrite auth_both_validI bi.and_elim_l.
     apply bi.exist_elim=> -[[c|]|];
@@ -242,7 +249,7 @@ Section gmap_view.
   Implicit Types (m : gmap K V) (k : K) (dq : dfrac) (v : V).
 
   Lemma gmap_view_both_validI m k dq v :
-    ✓ (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ⊢@{uPredI M}
+    ✓ (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ⊢
     ✓ dq ∧ m !! k ≡ Some v.
   Proof.
     rewrite /gmap_view_auth /gmap_view_frag. apply view_both_validI_1.
@@ -250,7 +257,7 @@ Section gmap_view.
   Qed.
 
   Lemma gmap_view_frag_op_validI k dq1 dq2 v1 v2 :
-    ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ⊣⊢@{uPredI M}
+    ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ⊣⊢
     ✓ (dq1 ⋅ dq2) ∧ v1 ≡ v2.
   Proof.
     rewrite /gmap_view_frag -view_frag_op. apply view_frag_validI=> n x.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index b3f0cee87069a59a0f5b64e50a8e2832f1854a85..3bcb256e3c37a2320ba33ff02897bed909320a86 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1,4 +1,5 @@
 From iris.bi Require Export bi.
+From iris.algebra Require Import frac.
 From iris.base_logic Require Export bi.
 From iris Require Import options.
 Import bi.bi base_logic.bi.uPred.
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index ab3325748ebf2f5f0b26db573e1bc048186dc2eb..f0b3719daab960d4571842c57e7329b714a3e9a0 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -44,8 +44,8 @@ Section proofs.
     AsFractional (cinv_own γ q) (cinv_own γ) q.
   Proof. split. done. apply _. Qed.
 
-  Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 -∗ cinv_own γ q2 -∗ ✓ (q1 + q2)%Qp.
-  Proof. apply (own_valid_2 γ q1 q2). Qed.
+  Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 -∗ cinv_own γ q2 -∗ ⌜q1 + q2 ≤ 1⌝%Qp.
+  Proof. rewrite -frac_validI. apply (own_valid_2 γ q1 q2). Qed.
 
   Lemma cinv_own_1_l γ q : cinv_own γ 1 -∗ cinv_own γ q -∗ False.
   Proof.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 634dae11f1cd52335262a2d89d19474b7747c6cb..ac6140a6602e0d055f987f85829de9e38da70035 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -157,12 +157,12 @@ Section gen_heap.
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
   Proof. split. done. apply _. Qed.
 
-  Lemma mapsto_valid l q v : l ↦{q} v -∗ ✓ q.
+  Lemma mapsto_valid l q v : l ↦{q} v -∗ ⌜q ≤ 1⌝%Qp.
   Proof.
     rewrite mapsto_eq. iIntros "Hl".
     iDestruct (own_valid with "Hl") as %?%gmap_view_frag_valid. done.
   Qed.
-  Lemma mapsto_valid_2 l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜✓ (q1 + q2)%Qp ∧ v1 = v2⌝.
+  Lemma mapsto_valid_2 l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ v1 = v2⌝.
   Proof.
     rewrite mapsto_eq. iIntros "H1 H2".
     iDestruct (own_valid_2 with "H1 H2") as %[??]%gmap_view_frag_op_valid_L.
@@ -184,7 +184,7 @@ Section gen_heap.
   Qed.
 
   Lemma mapsto_mapsto_ne l1 l2 q1 q2 v1 v2 :
-    ¬ ✓(q1 + q2)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
+    ¬ (q1 + q2 ≤ 1)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
   Proof.
     iIntros (?) "Hl1 Hl2"; iIntros (->).
     by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[??].
diff --git a/theories/base_logic/lib/ghost_var.v b/theories/base_logic/lib/ghost_var.v
index b4f6bc80e8487e9cf1fe42164e7828bdf35e6949..0632b0c24f6ce076358239442e0a486d7ccb28e5 100644
--- a/theories/base_logic/lib/ghost_var.v
+++ b/theories/base_logic/lib/ghost_var.v
@@ -44,7 +44,7 @@ Section lemmas.
   Proof. iApply own_alloc. done. Qed.
 
   Lemma ghost_var_valid_2 γ a1 q1 a2 q2 :
-    ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 -∗ ⌜✓ (q1 + q2)%Qp ∧ a1 = a2⌝.
+    ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ a1 = a2⌝.
   Proof.
     iIntros "Hvar1 Hvar2".
     iDestruct (own_valid_2 with "Hvar1 Hvar2") as %[Hq Ha]%frac_agree_op_valid.
diff --git a/theories/base_logic/lib/mnat.v b/theories/base_logic/lib/mnat.v
index 24962413800bf3de42895bf3aca71d32f2de644e..9773e4fafcd3fa263d20171b60d75b275b416dab 100644
--- a/theories/base_logic/lib/mnat.v
+++ b/theories/base_logic/lib/mnat.v
@@ -44,7 +44,7 @@ Section mnat.
   Proof. split; [auto|apply _]. Qed.
 
   Lemma mnat_own_auth_agree γ q1 q2 n1 n2 :
-    mnat_own_auth γ q1 n1 -∗ mnat_own_auth γ q2 n2 -∗ ⌜✓ (q1 + q2)%Qp ∧ n1 = n2⌝.
+    mnat_own_auth γ q1 n1 -∗ mnat_own_auth γ q2 n2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ n1 = n2⌝.
   Proof.
     iIntros "H1 H2".
     iDestruct (own_valid_2 with "H1 H2") as %?%mnat_auth_frac_op_valid; done.
@@ -58,7 +58,7 @@ Section mnat.
   Qed.
 
   Lemma mnat_own_lb_valid γ q n m :
-    mnat_own_auth γ q n -∗ mnat_own_lb γ m -∗ ⌜✓ q ∧ m ≤ n⌝.
+    mnat_own_auth γ q n -∗ mnat_own_lb γ m -∗ ⌜(q ≤ 1)%Qp ∧ m ≤ n⌝.
   Proof.
     iIntros "Hauth Hlb".
     iDestruct (own_valid_2 with "Hauth Hlb") as %Hvalid%mnat_auth_both_frac_valid.
diff --git a/theories/heap_lang/primitive_laws.v b/theories/heap_lang/primitive_laws.v
index 8d50d9d91d8743798bb2e163ee33ea06501b6bdc..afb76b7dbb5aca8d66c8e01465ae8576759c5cbe 100644
--- a/theories/heap_lang/primitive_laws.v
+++ b/theories/heap_lang/primitive_laws.v
@@ -277,12 +277,13 @@ Qed.
 (** We need to adjust the [gen_heap] and [gen_inv_heap] lemmas because of our
 value type being [option val]. *)
 
+Lemma mapsto_valid l q v : l ↦{q} v -∗ ⌜q ≤ 1⌝%Qp.
+Proof. apply mapsto_valid. Qed.
 Lemma mapsto_valid_2 l q1 q2 v1 v2 :
-  l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜✓ (q1 + q2)%Qp ∧ v1 = v2⌝.
+  l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ v1 = v2⌝.
 Proof.
   iIntros "H1 H2". iDestruct (mapsto_valid_2 with "H1 H2") as %[? [=?]]. done.
 Qed.
-
 Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜v1 = v2⌝.
 Proof. iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %[=?]. done. Qed.
 
@@ -293,10 +294,8 @@ Proof.
   iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
 Qed.
 
-Lemma mapsto_valid l q v : l ↦{q} v -∗ ✓ q.
-Proof. apply mapsto_valid. Qed.
 Lemma mapsto_mapsto_ne l1 l2 q1 q2 v1 v2 :
-  ¬ ✓(q1 + q2)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
+  ¬ (q1 + q2 ≤ 1)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
 Proof. apply mapsto_mapsto_ne. Qed.
 
 Global Instance inv_mapsto_own_proper l v :