diff --git a/iris/algebra/auth.v b/iris/algebra/auth.v
index 702b0b33b30d241ec3f668aafdbcae3e20bd03b4..fe102666fd297fcc1a29bc4d7dbb7fb485f25cb0 100644
--- a/iris/algebra/auth.v
+++ b/iris/algebra/auth.v
@@ -3,12 +3,13 @@ From iris.algebra Require Import proofmode_classes big_op.
 From iris.prelude Require Import options.
 
 (** The authoritative camera with fractional authoritative elements *)
-(** The authoritative camera has 2 types of elements: the authoritative
-element [●{q} a] and the fragment [◯ b] (of which there can be several). To
-enable sharing of the authoritative element [●{q} a], it is equiped with a
-fraction [q]. Updates are only possible with the full authoritative element
-[● a] (syntax for [●{1} a]]), while fractional authoritative elements have
-agreement, i.e., [✓ (●{p1} a1 ⋅ ●{p2} a2) → a1 ≡ a2]. *)
+(** The authoritative camera has 2 types of elements: the authoritative element
+[●{dq} a] and the fragment [◯ b] (of which there can be several). To enable
+sharing of the authoritative element [●{dq} a], it is equiped with a
+discardable fraction [dq]. Updates are only possible with the full
+authoritative element [● a] (syntax for [●{#1} a]]), while fractional
+authoritative elements have agreement, i.e., [✓ (●{dq1} a1 ⋅ ●{dq2} a2) → a1 ≡
+a2]. *)
 
 (** * Definition of the view relation *)
 (** The authoritative camera is obtained by instantiating the view camera. *)
@@ -61,7 +62,7 @@ Definition authO (A : ucmra) : ofe := viewO (A:=A) (B:=A) auth_view_rel.
 Definition authR (A : ucmra) : cmra := viewR (A:=A) (B:=A) auth_view_rel.
 Definition authUR (A : ucmra) : ucmra := viewUR (A:=A) (B:=A) auth_view_rel.
 
-Definition auth_auth {A: ucmra} : Qp → A → auth A := view_auth.
+Definition auth_auth {A: ucmra} : dfrac → A → auth A := view_auth.
 Definition auth_frag {A: ucmra} : A → auth A := view_frag.
 
 Typeclasses Opaque auth_auth auth_frag.
@@ -69,9 +70,13 @@ Typeclasses Opaque auth_auth auth_frag.
 Global Instance: Params (@auth_auth) 2 := {}.
 Global Instance: Params (@auth_frag) 1 := {}.
 
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
+Notation "●{ dq } a" := (auth_auth dq a) (at level 20, format "●{ dq }  a").
+Notation "●{# q } a" := (auth_auth (DfracOwn q) a) (at level 20, format "●{# q }  a").
+Notation "●□ a" := (auth_auth (DfracDiscarded) a) (at level 20).
+Notation "● a" := (auth_auth (DfracOwn 1) a) (at level 20).
 Notation "â—¯ a" := (auth_frag a) (at level 20).
-Notation "●{ q } a" := (auth_auth q a) (at level 20, format "●{ q }  a").
-Notation "● a" := (auth_auth 1 a) (at level 20).
 
 (** * Laws of the authoritative camera *)
 (** We omit the usual [equivI] lemma because it is hard to state a suitably
@@ -82,9 +87,9 @@ Section auth.
   Implicit Types a b : A.
   Implicit Types x y : auth A.
 
-  Global Instance auth_auth_ne q : NonExpansive (@auth_auth A q).
+  Global Instance auth_auth_ne dq : NonExpansive (@auth_auth A dq).
   Proof. rewrite /auth_auth. apply _. Qed.
-  Global Instance auth_auth_proper q : Proper ((≡) ==> (≡)) (@auth_auth A q).
+  Global Instance auth_auth_proper dq : Proper ((≡) ==> (≡)) (@auth_auth A dq).
   Proof. rewrite /auth_auth. apply _. Qed.
   Global Instance auth_frag_ne : NonExpansive (@auth_frag A).
   Proof. rewrite /auth_frag. apply _. Qed.
@@ -102,8 +107,8 @@ Section auth.
 
   Global Instance auth_ofe_discrete : OfeDiscrete A → OfeDiscrete (authO A).
   Proof. apply _. Qed.
-  Global Instance auth_auth_discrete q a :
-    Discrete a → Discrete (ε : A) → Discrete (●{q} a).
+  Global Instance auth_auth_discrete dq a :
+    Discrete a → Discrete (ε : A) → Discrete (●{dq} a).
   Proof. rewrite /auth_auth. apply _. Qed.
   Global Instance auth_frag_discrete a : Discrete a → Discrete (◯ a).
   Proof. rewrite /auth_frag. apply _. Qed.
@@ -111,10 +116,10 @@ Section auth.
   Proof. apply _. Qed.
 
   (** Operation *)
-  Lemma auth_auth_frac_op p q a : ●{p + q} a ≡ ●{p} a ⋅ ●{q} a.
+  Lemma auth_auth_frac_op dq1 dq2 a : ●{dq1 ⋅ dq2} a ≡ ●{dq1} a ⋅ ●{dq2} a.
   Proof. apply view_auth_frac_op. Qed.
-  Global Instance auth_auth_frac_is_op q q1 q2 a :
-    IsOp q q1 q2 → IsOp' (●{q} a) (●{q1} a) (●{q2} a).
+  Global Instance auth_auth_frac_is_op dq dq1 dq2 a :
+    IsOp dq dq1 dq2 → IsOp' (●{dq} a) (●{dq1} a) (●{dq2} a).
   Proof. rewrite /auth_auth. apply _. Qed.
 
   Lemma auth_frag_op a b : â—¯ (a â‹… b) = â—¯ a â‹… â—¯ b.
@@ -146,21 +151,21 @@ Section auth.
   Proof. apply (big_opMS_commute _). Qed.
 
   (** Validity *)
-  Lemma auth_auth_frac_op_invN n p a q b : ✓{n} (●{p} a ⋅ ●{q} b) → a ≡{n}≡ b.
+  Lemma auth_auth_frac_op_invN n dq1 a dq2 b : ✓{n} (●{dq1} a ⋅ ●{dq2} b) → a ≡{n}≡ b.
   Proof. apply view_auth_frac_op_invN. Qed.
-  Lemma auth_auth_frac_op_inv p a q b : ✓ (●{p} a ⋅ ●{q} b) → a ≡ b.
+  Lemma auth_auth_frac_op_inv dq1 a dq2 b : ✓ (●{dq1} a ⋅ ●{dq2} b) → a ≡ b.
   Proof. apply view_auth_frac_op_inv. Qed.
-  Lemma auth_auth_frac_op_inv_L `{!LeibnizEquiv A} q a p b :
-    ✓ (●{p} a ⋅ ●{q} b) → a = b.
+  Lemma auth_auth_frac_op_inv_L `{!LeibnizEquiv A} dq1 a dq2 b :
+    ✓ (●{dq1} a ⋅ ●{dq2} b) → a = b.
   Proof. by apply view_auth_frac_op_inv_L. Qed.
 
-  Lemma auth_auth_frac_validN n q a : ✓{n} (●{q} a) ↔ (q ≤ 1)%Qp ∧ ✓{n} a.
+  Lemma auth_auth_frac_validN n dq a : ✓{n} (●{dq} a) ↔ ✓dq ∧ ✓{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 ≤ 1)%Qp ∧ a1 ≡{n}≡ a2 ∧ ✓{n} a1.
+    ✓{n} (●{q1} a1 ⋅ ●{q2} a2) ↔  ✓(q1 ⋅ q2) ∧ 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.
@@ -180,13 +185,13 @@ Section auth.
   Lemma auth_frag_op_validN_2 n b1 b2 : ✓{n} (b1 ⋅ b2) → ✓{n} (◯ b1 ⋅ ◯ b2).
   Proof. apply auth_frag_op_validN. Qed.
 
-  Lemma auth_both_frac_validN n q a b :
-    ✓{n} (●{q} a ⋅ ◯ b) ↔ (q ≤ 1)%Qp ∧ b ≼{n} a ∧ ✓{n} a.
+  Lemma auth_both_frac_validN n dq a b :
+    ✓{n} (●{dq} a ⋅ ◯ b) ↔ ✓dq ∧ 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 ≤ 1)%Qp ∧ ✓ a.
+  Lemma auth_auth_frac_valid dq a : ✓ (●{dq} a) ↔ ✓dq ∧ ✓ a.
   Proof.
     rewrite view_auth_frac_valid !cmra_valid_validN.
     by setoid_rewrite auth_view_rel_unit.
@@ -198,7 +203,7 @@ Section auth.
   Qed.
 
   Lemma auth_auth_frac_op_valid q1 q2 a1 a2 :
-    ✓ (●{q1} a1 ⋅ ●{q2} a2) ↔ (q1 + q2 ≤ 1)%Qp ∧ a1 ≡ a2 ∧ ✓ a1.
+    ✓ (●{q1} a1 ⋅ ●{q2} a2) ↔ ✓(q1 ⋅ q2) ∧ a1 ≡ a2 ∧ ✓ a1.
   Proof.
     rewrite view_auth_frac_op_valid !cmra_valid_validN.
     setoid_rewrite auth_view_rel_unit. done.
@@ -227,8 +232,8 @@ Section auth.
   (** These lemma statements are a bit awkward as we cannot possibly extract a
   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 ≤ 1)%Qp ∧ (∀ n, b ≼{n} a) ∧ ✓ a.
+  Lemma auth_both_frac_valid dq a b :
+    ✓ (●{dq} a ⋅ ◯ b) ↔  ✓dq ∧ (∀ n, b ≼{n} a) ∧ ✓ a.
   Proof.
     rewrite view_both_frac_valid. apply and_iff_compat_l. split.
     - intros Hrel. split.
@@ -238,11 +243,11 @@ Section auth.
   Qed.
   Lemma auth_both_valid a b :
     ✓ (● a ⋅ ◯ b) ↔ (∀ n, b ≼{n} a) ∧ ✓ a.
-  Proof. rewrite auth_both_frac_valid. naive_solver. Qed.
+  Proof. rewrite auth_both_frac_valid. split; [naive_solver|done]. 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 ≤ 1)%Qp → ✓ a → b ≼ a → ✓ (●{q} a ⋅ ◯ b).
+  Lemma auth_both_frac_valid_2 dq a b : ✓dq → ✓ a → b ≼ a → ✓ (●{dq} a ⋅ ◯ b).
   Proof.
     intros. apply auth_both_frac_valid.
     naive_solver eauto using cmra_included_includedN.
@@ -250,22 +255,22 @@ Section auth.
   Lemma auth_both_valid_2 a b : ✓ a → b ≼ a → ✓ (● a ⋅ ◯ b).
   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 ≤ 1)%Qp ∧ b ≼ a ∧ ✓ a.
+  Lemma auth_both_frac_valid_discrete `{!CmraDiscrete A} dq a b :
+    ✓ (●{dq} a ⋅ ◯ b) ↔ ✓dq ∧ 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. naive_solver. Qed.
+  Proof. rewrite auth_both_frac_valid_discrete. split; [naive_solver|done]. Qed.
 
   (** Inclusion *)
-  Lemma auth_auth_frac_includedN n p1 p2 a1 a2 b :
-    ●{p1} a1 ≼{n} ●{p2} a2 ⋅ ◯ b ↔ (p1 ≤ p2)%Qp ∧ a1 ≡{n}≡ a2.
+  Lemma auth_auth_frac_includedN n dq1 dq2 a1 a2 b :
+    ●{dq1} a1 ≼{n} ●{dq2} a2 ⋅ ◯ b ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡{n}≡ a2.
   Proof. apply view_auth_frac_includedN. Qed.
-  Lemma auth_auth_frac_included p1 p2 a1 a2 b :
-    ●{p1} a1 ≼ ●{p2} a2 ⋅ ◯ b ↔ (p1 ≤ p2)%Qp ∧ a1 ≡ a2.
+  Lemma auth_auth_frac_included dq1 dq2 a1 a2 b :
+    ●{dq1} a1 ≼ ●{dq2} a2 ⋅ ◯ b ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡ a2.
   Proof. apply view_auth_frac_included. Qed.
   Lemma auth_auth_includedN n a1 a2 b :
     ● a1 ≼{n} ● a2 ⋅ ◯ b ↔ a1 ≡{n}≡ a2.
@@ -274,20 +279,20 @@ Section auth.
     ● a1 ≼ ● a2 ⋅ ◯ b ↔ a1 ≡ a2.
   Proof. apply view_auth_included. Qed.
 
-  Lemma auth_frag_includedN n p a b1 b2 :
-    ◯ b1 ≼{n} ●{p} a ⋅ ◯ b2 ↔ b1 ≼{n} b2.
+  Lemma auth_frag_includedN n dq a b1 b2 :
+    ◯ b1 ≼{n} ●{dq} a ⋅ ◯ b2 ↔ b1 ≼{n} b2.
   Proof. apply view_frag_includedN. Qed.
-  Lemma auth_frag_included p a b1 b2 :
-    ◯ b1 ≼ ●{p} a ⋅ ◯ b2 ↔ b1 ≼ b2.
+  Lemma auth_frag_included dq a b1 b2 :
+    ◯ b1 ≼ ●{dq} a ⋅ ◯ b2 ↔ b1 ≼ b2.
   Proof. apply view_frag_included. Qed.
 
   (** The weaker [auth_both_included] lemmas below are a consequence of the
   [auth_auth_included] and [auth_frag_included] lemmas above. *)
-  Lemma auth_both_frac_includedN n p1 p2 a1 a2 b1 b2 :
-    ●{p1} a1 ⋅ ◯ b1 ≼{n} ●{p2} a2 ⋅ ◯ b2 ↔ (p1 ≤ p2)%Qp ∧ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
+  Lemma auth_both_frac_includedN n dq1 dq2 a1 a2 b1 b2 :
+    ●{dq1} a1 ⋅ ◯ b1 ≼{n} ●{dq2} a2 ⋅ ◯ b2 ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
   Proof. apply view_both_frac_includedN. Qed.
-  Lemma auth_both_frac_included p1 p2 a1 a2 b1 b2 :
-    ●{p1} a1 ⋅ ◯ b1 ≼ ●{p2} a2 ⋅ ◯ b2 ↔ (p1 ≤ p2)%Qp ∧ a1 ≡ a2 ∧ b1 ≼ b2.
+  Lemma auth_both_frac_included dq1 dq2 a1 a2 b1 b2 :
+    ●{dq1} a1 ⋅ ◯ b1 ≼ ●{dq2} a2 ⋅ ◯ b2 ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡ a2 ∧ b1 ≼ b2.
   Proof. apply view_both_frac_included. Qed.
   Lemma auth_both_includedN n a1 a2 b1 b2 :
     ● a1 ⋅ ◯ b1 ≼{n} ● a2 ⋅ ◯ b2 ↔ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
@@ -314,9 +319,11 @@ Section auth.
     intros. etrans; first exact: auth_update_alloc.
     exact: cmra_update_op_l.
   Qed.
+  Lemma auth_update_auth_persist dq a : ●{dq} a ~~> ●□ a.
+  Proof. apply view_update_auth_persist. Qed.
 
-  Lemma auth_update_frac_alloc q a b `{!CoreId b} :
-    b ≼ a → ●{q} a ~~> ●{q} a ⋅ ◯ b.
+  Lemma auth_update_frac_alloc dq a b `{!CoreId b} :
+    b ≼ a → ●{dq} a ~~> ●{dq} a ⋅ ◯ b.
   Proof.
     intros Ha%(core_id_extract _ _). apply view_update_frac_alloc=> n bf [??].
     split; [|done]. rewrite Ha (comm _ a). by apply cmra_monoN_l.
diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index e0329dbe3c7b8252770aaaf1caed39b58ad9358f..f38afd0e4f0eb0c2c05cb4755ba6add697fcd2f1 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -153,7 +153,7 @@ Section dfrac.
     - by destruct (Qp_add_id_free q q2).
     - by destruct (Qp_add_id_free q q1).
   Qed.
-  Global Instance frac_id_free q : IdFree (DfracOwn q).
+  Global Instance dfrac_own_id_free q : IdFree (DfracOwn q).
   Proof. intros [q'| |q'] _ [=]. by apply (Qp_add_id_free q q'). Qed.
   Global Instance dfrac_discarded_core_id : CoreId DfracDiscarded.
   Proof. by constructor. Qed.
diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index a2b8591e4b9893edac23db48c99936e01c8ac173..7b27e2c4f2e7a0bcd43a93c7b6b3e59b73b08c74 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -1,5 +1,5 @@
 From Coq.QArith Require Import Qcanon.
-From iris.algebra Require Export view gmap dfrac.
+From iris.algebra Require Export view gmap frac dfrac.
 From iris.algebra Require Import local_updates proofmode_classes big_op.
 From iris.prelude Require Import options.
 
@@ -12,7 +12,7 @@ persistent read-only ownership of a key.
 
 The key frame-preserving updates are [gmap_view_alloc] to allocate a new key,
 [gmap_view_update] to update a key given full ownership of the corresponding
-fragment, and [gmap_view_freeze] to make a key read-only by discarding any
+fragment, and [gmap_view_persist] to make a key read-only by discarding any
 fraction of the corresponding fragment. Crucially, the latter does not require
 owning the authoritative element.
 
@@ -138,7 +138,7 @@ Section definitions.
   Context {K : Type} `{Countable K} {V : ofe}.
 
   Definition gmap_view_auth (q : frac) (m : gmap K V) : gmap_viewR K V :=
-    ●V{q} m.
+    ●V{#q} m.
   Definition gmap_view_frag (k : K) (dq : dfrac) (v : V) : gmap_viewR K V :=
     â—¯V {[k := (dq, to_agree v)]}.
 End definitions.
@@ -178,7 +178,7 @@ Section lemmas.
   (** Composition and validity *)
   Lemma gmap_view_auth_frac_op p q m :
     gmap_view_auth (p + q) m ≡ gmap_view_auth p m ⋅ gmap_view_auth q m.
-  Proof. apply view_auth_frac_op. Qed.
+  Proof. by rewrite /gmap_view_auth -dfrac_op_own view_auth_frac_op. Qed.
   Global Instance gmap_view_auth_frac_is_op q q1 q2 m :
     IsOp q q1 q2 → IsOp' (gmap_view_auth q m) (gmap_view_auth q1 m) (gmap_view_auth q2 m).
   Proof. rewrite /gmap_view_auth. apply _. Qed.
diff --git a/iris/algebra/lib/gset_bij.v b/iris/algebra/lib/gset_bij.v
index 7011f8ca0a22629e79548afaeb92f21d661a2362..b4d7d4b731a4d6e37e22262808676b8fe7338e5b 100644
--- a/iris/algebra/lib/gset_bij.v
+++ b/iris/algebra/lib/gset_bij.v
@@ -106,7 +106,7 @@ Definition gset_bijUR A B `{Countable A, Countable B} : ucmra :=
   viewUR (gset_bij_view_rel (A:=A) (B:=B)).
 
 Definition gset_bij_auth `{Countable A, Countable B}
-  (q : Qp) (L : gset (A * B)) : gset_bij A B := ●V{q} L ⋅ ◯V L.
+  (dq : dfrac) (L : gset (A * B)) : gset_bij A B := ●V{dq} L ⋅ ◯V L.
 Definition gset_bij_elem `{Countable A, Countable B}
   (a : A) (b : B) : gset_bij A B := â—¯V {[a, b]}.
 
@@ -118,11 +118,11 @@ Section gset_bij.
   Global Instance gset_bij_elem_core_id a b : CoreId (gset_bij_elem a b).
   Proof. apply _. Qed.
 
-  Lemma gset_bij_auth_frac_op q1 q2 L :
-    gset_bij_auth q1 L ⋅ gset_bij_auth q2 L ≡ gset_bij_auth (q1 + q2) L.
+  Lemma gset_bij_auth_frac_op dq1 dq2 L :
+    gset_bij_auth dq1 L ⋅ gset_bij_auth dq2 L ≡ gset_bij_auth (dq1 ⋅ dq2) L.
   Proof.
     rewrite /gset_bij_auth view_auth_frac_op.
-    rewrite (comm _ (●V{q2} _)) -!assoc (assoc _ (◯V _)).
+    rewrite (comm _ (●V{dq2} _)) -!assoc (assoc _ (◯V _)).
     by rewrite -core_id_dup (comm _ (â—¯V _)).
   Qed.
 
@@ -132,21 +132,21 @@ Section gset_bij.
     setoid_rewrite gset_bij_view_rel_iff.
     naive_solver eauto using O.
   Qed.
-  Lemma gset_bij_auth_valid L : ✓ gset_bij_auth 1 L ↔ gset_bijective L.
+  Lemma gset_bij_auth_valid L : ✓ gset_bij_auth (DfracOwn 1) L ↔ gset_bijective L.
   Proof. rewrite gset_bij_auth_frac_valid. naive_solver by done. Qed.
 
   Lemma gset_bij_auth_empty_frac_valid q : ✓ gset_bij_auth (A:=A) (B:=B) q ∅ ↔ ✓ q.
   Proof.
     rewrite gset_bij_auth_frac_valid. naive_solver eauto using gset_bijective_empty.
   Qed.
-  Lemma gset_bij_auth_empty_valid : ✓ gset_bij_auth (A:=A) (B:=B) 1 ∅.
+  Lemma gset_bij_auth_empty_valid : ✓ gset_bij_auth (A:=A) (B:=B) (DfracOwn 1) ∅.
   Proof. by apply gset_bij_auth_empty_frac_valid. Qed.
 
-  Lemma gset_bij_auth_frac_op_valid q1 q2 L1 L2 :
-    ✓ (gset_bij_auth q1 L1 ⋅ gset_bij_auth q2 L2)
-    ↔ ✓ (q1 + q2)%Qp ∧ L1 = L2 ∧ gset_bijective L1.
+  Lemma gset_bij_auth_frac_op_valid dq1 dq2 L1 L2 :
+    ✓ (gset_bij_auth dq1 L1 ⋅ gset_bij_auth dq2 L2)
+    ↔ ✓ (dq1 ⋅ dq2) ∧ L1 = L2 ∧ gset_bijective L1.
   Proof.
-    rewrite /gset_bij_auth (comm _ (●V{q2} _)) -!assoc (assoc _ (◯V _)).
+    rewrite /gset_bij_auth (comm _ (●V{dq2} _)) -!assoc (assoc _ (◯V _)).
     rewrite -view_frag_op (comm _ (â—¯V _)) assoc. split.
     - move=> /cmra_valid_op_l /view_auth_frac_op_valid.
       setoid_rewrite gset_bij_view_rel_iff. naive_solver eauto using 0.
@@ -154,7 +154,7 @@ Section gset_bij.
       apply view_both_frac_valid. setoid_rewrite gset_bij_view_rel_iff. naive_solver.
   Qed.
   Lemma gset_bij_auth_op_valid L1 L2 :
-    ✓ (gset_bij_auth 1 L1 ⋅ gset_bij_auth 1 L2) ↔ False.
+    ✓ (gset_bij_auth (DfracOwn 1) L1 ⋅ gset_bij_auth (DfracOwn 1) L2) ↔ False.
   Proof. rewrite gset_bij_auth_frac_op_valid. naive_solver. Qed.
 
   Lemma bij_both_frac_valid q L a b :
@@ -165,7 +165,7 @@ Section gset_bij.
     set_solver by eauto using O.
   Qed.
   Lemma bij_both_valid L a b :
-    ✓ (gset_bij_auth 1 L ⋅ gset_bij_elem a b) ↔ gset_bijective L ∧ (a, b) ∈ L.
+    ✓ (gset_bij_auth (DfracOwn 1) L ⋅ gset_bij_elem a b) ↔ gset_bijective L ∧ (a, b) ∈ L.
   Proof. rewrite bij_both_frac_valid. naive_solver by done. Qed.
 
   Lemma gset_bij_elem_agree a1 b1 a2 b2 :
@@ -185,7 +185,7 @@ Section gset_bij.
 
   Lemma gset_bij_auth_extend {L} a b :
     (∀ b', (a, b') ∉ L) → (∀ a', (a', b) ∉ L) →
-    gset_bij_auth 1 L ~~> gset_bij_auth 1 ({[(a, b)]} ∪ L).
+    gset_bij_auth (DfracOwn 1) L ~~> gset_bij_auth (DfracOwn 1) ({[(a, b)]} ∪ L).
   Proof.
     intros. apply view_update=> n bijL.
     rewrite !gset_bij_view_rel_iff gset_op.
diff --git a/iris/algebra/lib/mono_nat.v b/iris/algebra/lib/mono_nat.v
index d7d312caa50e89619c5a8d42660bedf5ce18bcae..b8ee6dd0b7c3dd984842667afc3637ce63c15b99 100644
--- a/iris/algebra/lib/mono_nat.v
+++ b/iris/algebra/lib/mono_nat.v
@@ -14,7 +14,7 @@ fragment at the same value so that lemma [mono_nat_included], which states that
 [mono_nat_lb n ≼ mono_nat_auth q n], does not require a frame-preserving
 update. *)
 Definition mono_nat_auth (q : Qp) (n : nat) : mono_nat :=
-  ●{q} MaxNat n ⋅ ◯ MaxNat n.
+  ●{#q} MaxNat n ⋅ ◯ MaxNat n.
 Definition mono_nat_lb (n : nat) : mono_nat := â—¯ MaxNat n.
 
 Section mono_nat.
@@ -26,8 +26,8 @@ Section mono_nat.
   Lemma mono_nat_auth_frac_op q1 q2 n :
     mono_nat_auth q1 n ⋅ mono_nat_auth q2 n ≡ mono_nat_auth (q1 + q2) n.
   Proof.
-    rewrite /mono_nat_auth auth_auth_frac_op.
-    rewrite (comm _ (●{q2} _)) -!assoc (assoc _ (◯ _)).
+    rewrite /mono_nat_auth -dfrac_op_own auth_auth_frac_op.
+    rewrite (comm _ (●{#q2} _)) -!assoc (assoc _ (◯ _)).
     by rewrite -core_id_dup (comm _ (â—¯ _)).
   Qed.
 
@@ -60,7 +60,7 @@ Section mono_nat.
   Lemma mono_nat_auth_frac_op_valid q1 q2 n1 n2 :
     ✓ (mono_nat_auth q1 n1 ⋅ mono_nat_auth q2 n2) ↔ (q1 + q2 ≤ 1)%Qp ∧ n1 = n2.
   Proof.
-    rewrite /mono_nat_auth (comm _ (●{q2} _)) -!assoc (assoc _ (◯ _)).
+    rewrite /mono_nat_auth (comm _ (●{#q2} _)) -!assoc (assoc _ (◯ _)).
     rewrite -auth_frag_op (comm _ (â—¯ _)) assoc. split.
     - move=> /cmra_valid_op_l /auth_auth_frac_op_valid. naive_solver.
     - intros [? ->]. rewrite -core_id_dup -auth_auth_frac_op.
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 47ecc5bdca7e99b624349c817e4ad924a37e77fa..b265f5db9f72304a28de5bcf7a77d6c7fc5188be 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -1,13 +1,13 @@
-From iris.algebra Require Export updates local_updates frac agree.
+From iris.algebra Require Export updates local_updates dfrac agree.
 From iris.algebra Require Import proofmode_classes big_op.
 From iris.prelude Require Import options.
 
 (** The view camera with fractional authoritative elements *)
 (** The view camera, which is reminiscent of the views framework, is used to
-provide a logical/"small-footprint" "view" of some "large-footprint" piece of
-data, which can be shared in the separation logic sense, i.e., different parts
-of the data can be separately owned by different functions or threads. This is
-achieved using the two elements of the view camera:
+  provide a logical/"small-footprint" "view" of some "large-footprint" piece of
+  data, which can be shared in the separation logic sense, i.e., different parts
+  of the data can be separately owned by different functions or threads. This is
+  achieved using the two elements of the view camera:
 
 - The authoritative element [●V a], which describes the data under consideration.
 - The fragment [â—¯V b], which provides a logical view of the data [a].
@@ -16,10 +16,10 @@ To enable sharing of the fragments, the type of fragments is equipped with a
 camera structure so ownership of fragments can be split. Concretely, fragments
 enjoy the rule [â—¯V (b1 â‹… b2) = â—¯V b1 â‹… â—¯V b2].
 
-To enable sharing of the authoritative element [●V{q} a], it is equipped with a
-fraction [q]. Updates are only possible with the full authoritative element
-[●V a] (syntax for [●V{1} a]]), while fractional authoritative elements have
-agreement, i.e., [✓ (●V{p1} a1 ⋅ ●V{p2} a2) → a1 ≡ a2]. *)
+To enable sharing of the authoritative element [●V{dq} a], it is equipped with a
+discardable fraction [dq]. Updates are only possible with the full authoritative
+element [●V a] (syntax for [●V{#1} a]]), while fractional authoritative elements
+have agreement, i.e., [✓ (●V{dq1} a1 ⋅ ●V{dq2} a2) → a1 ≡ a2]. *)
 
 (** * The view relation *)
 (** To relate the authoritative element [a] to its possible fragments [b], the
@@ -75,7 +75,7 @@ Class ViewRelDiscrete {A B} (rel : view_rel A B) :=
 always be constructed using [●V] and [◯V], and never using the constructor
 [View]. *)
 Record view {A B} (rel : nat → A → B → Prop) :=
-  View { view_auth_proj : option (frac * agree A) ; view_frag_proj : B }.
+  View { view_auth_proj : option (dfrac * agree A) ; view_frag_proj : B }.
 Add Printing Constructor view.
 Global Arguments View {_ _ _} _ _.
 Global Arguments view_auth_proj {_ _ _} _.
@@ -84,16 +84,20 @@ Global Instance: Params (@View) 3 := {}.
 Global Instance: Params (@view_auth_proj) 3 := {}.
 Global Instance: Params (@view_frag_proj) 3 := {}.
 
-Definition view_auth {A B} {rel : view_rel A B} (q : Qp) (a : A) : view rel :=
-  View (Some (q, to_agree a)) ε.
+Definition view_auth {A B} {rel : view_rel A B} (dq : dfrac) (a : A) : view rel :=
+  View (Some (dq, to_agree a)) ε.
 Definition view_frag {A B} {rel : view_rel A B} (b : B) : view rel := View None b.
 Typeclasses Opaque view_auth view_frag.
 
 Global Instance: Params (@view_auth) 3 := {}.
 Global Instance: Params (@view_frag) 3 := {}.
 
-Notation "●V{ q } a" := (view_auth q a) (at level 20, format "●V{ q }  a").
-Notation "●V a" := (view_auth 1 a) (at level 20).
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
+Notation "●V{ dq } a" := (view_auth dq a) (at level 20, format "●V{ dq }  a").
+Notation "●V{# q } a" := (view_auth (DfracOwn q) a) (at level 20, format "●V{# q }  a").
+Notation "●V□ a" := (view_auth DfracDiscarded a) (at level 20, format "●V□  a").
+Notation "●V a" := (view_auth (DfracOwn 1) a) (at level 20).
 Notation "â—¯V a" := (view_frag a) (at level 20).
 
 (** * The OFE structure *)
@@ -103,7 +107,7 @@ been needed in practice. *)
 Section ofe.
   Context {A B : ofe} (rel : nat → A → B → Prop).
   Implicit Types a : A.
-  Implicit Types ag : option (frac * agree A).
+  Implicit Types ag : option (dfrac * agree A).
   Implicit Types b : B.
   Implicit Types x y : view rel.
 
@@ -144,13 +148,13 @@ End ofe.
 Section cmra.
   Context {A B} (rel : view_rel A B).
   Implicit Types a : A.
-  Implicit Types ag : option (frac * agree A).
+  Implicit Types ag : option (dfrac * agree A).
   Implicit Types b : B.
   Implicit Types x y : view rel.
 
-  Global Instance view_auth_ne q : NonExpansive (@view_auth A B rel q).
+  Global Instance view_auth_ne dq : NonExpansive (@view_auth A B rel dq).
   Proof. solve_proper. Qed.
-  Global Instance view_auth_proper q : Proper ((≡) ==> (≡)) (@view_auth A B rel q).
+  Global Instance view_auth_proper dq : Proper ((≡) ==> (≡)) (@view_auth A B rel dq).
   Proof. solve_proper. Qed.
   Global Instance view_frag_ne : NonExpansive (@view_frag A B rel).
   Proof. done. Qed.
@@ -160,12 +164,12 @@ Section cmra.
   Global Instance view_auth_dist_inj n :
     Inj2 (=) (dist n) (dist n) (@view_auth A B rel).
   Proof.
-    intros p1 a1 p2 a2 [Hag ?]; inversion Hag as [?? [??]|]; simplify_eq/=.
+    intros dq1 a1 dq2 a2 [Hag ?]; inversion Hag as [?? [??]|]; simplify_eq/=.
     split; [done|]. by apply (inj to_agree).
   Qed.
   Global Instance view_auth_inj : Inj2 (=) (≡) (≡) (@view_auth A B rel).
   Proof.
-    intros p1 a1 p2 a2 [Hag ?]; inversion Hag as [?? [??]|]; simplify_eq/=.
+    intros dq1 a1 dq2 a2 [Hag ?]; inversion Hag as [?? [??]|]; simplify_eq/=.
     split; [done|]. by apply (inj to_agree).
   Qed.
   Global Instance view_frag_dist_inj n : Inj (dist n) (dist n) (@view_frag A B rel).
@@ -175,14 +179,14 @@ Section cmra.
 
   Local Instance view_valid_instance : Valid (view rel) := λ x,
     match view_auth_proj x with
-    | Some (q, ag) =>
-       ✓ q ∧ (∀ n, ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x))
+    | Some (dq, ag) =>
+       ✓ dq ∧ (∀ n, ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x))
     | None => ∀ n, ∃ a, rel n a (view_frag_proj x)
     end.
   Local Instance view_validN_instance : ValidN (view rel) := λ n x,
     match view_auth_proj x with
-    | Some (q, ag) =>
-       ✓{n} q ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x)
+    | Some (dq, ag) =>
+       ✓{n} dq ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x)
     | None => ∃ a, rel n a (view_frag_proj x)
     end.
   Local Instance view_pcore_instance : PCore (view rel) := λ x,
@@ -193,32 +197,32 @@ Section cmra.
   Local Definition view_valid_eq :
     valid = λ x,
       match view_auth_proj x with
-      | Some (q, ag) =>
-         ✓ q ∧ (∀ n, ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x))
+      | Some (dq, ag) =>
+         ✓ dq ∧ (∀ n, ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x))
       | None => ∀ n, ∃ a, rel n a (view_frag_proj x)
       end := eq_refl _.
   Local Definition view_validN_eq :
-    validN = λ n x, 
+    validN = λ n x,
       match view_auth_proj x with
-      | Some (q, ag) => ✓{n} q ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x)
+      | Some (dq, ag) => ✓{n} dq ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x)
       | None => ∃ a, rel n a (view_frag_proj x)
       end := eq_refl _.
 
   Lemma view_cmra_mixin : CmraMixin (view rel).
   Proof.
     apply (iso_cmra_mixin_restrict
-      (λ x : option (frac * agree A) * B, View x.1 x.2)
+      (λ x : option (dfrac * agree A) * B, View x.1 x.2)
       (λ x, (view_auth_proj x, view_frag_proj x))); try done.
     - intros [x b]. by rewrite /= pair_pcore !cmra_pcore_core.
-    - intros n [[[q ag]|] b]; rewrite /= view_validN_eq /=.
+    - intros n [[[dq ag]|] b]; rewrite /= view_validN_eq /=.
       + intros (?&a&->&?). repeat split; simpl; [done|]. by eapply view_rel_validN.
       + intros [a ?]. repeat split; simpl. by eapply view_rel_validN.
     - rewrite view_validN_eq.
       intros n [x1 b1] [x2 b2] [Hx ?]; simpl in *;
         destruct Hx as [[q1 ag1] [q2 ag2] [??]|]; intros ?; by ofe_subst.
     - rewrite view_valid_eq view_validN_eq.
-      intros [[[q aa]|] b]; rewrite /= ?cmra_valid_validN; naive_solver.
-    - rewrite view_validN_eq=> n [[[q ag]|] b] /=.
+      intros [[[dq aa]|] b]; rewrite /= ?cmra_valid_validN; naive_solver.
+    - rewrite view_validN_eq=> n [[[dq ag]|] b] /=.
       + intros [? (a&?&?)]; split; [done|].
         exists a; split; [by eauto using dist_S|].
         apply view_rel_mono with (S n) a b; auto with lia.
@@ -237,8 +241,8 @@ Section cmra.
   Qed.
   Canonical Structure viewR := Cmra (view rel) view_cmra_mixin.
 
-  Global Instance view_auth_discrete q a :
-    Discrete a → Discrete (ε : B) → Discrete (●V{q} a : view rel).
+  Global Instance view_auth_discrete dq a :
+    Discrete a → Discrete (ε : B) → Discrete (●V{dq} a : view rel).
   Proof. intros. apply View_discrete; apply _. Qed.
   Global Instance view_frag_discrete b :
     Discrete b → Discrete (◯V b : view rel).
@@ -247,7 +251,7 @@ Section cmra.
     OfeDiscrete A → CmraDiscrete B → ViewRelDiscrete rel →
     CmraDiscrete viewR.
   Proof.
-    split; [apply _|]=> -[[[q ag]|] b]; rewrite view_valid_eq view_validN_eq /=.
+    split; [apply _|]=> -[[[dq ag]|] b]; rewrite view_valid_eq view_validN_eq /=.
     - rewrite -cmra_discrete_valid_iff.
       setoid_rewrite <-(discrete_iff _ ag). naive_solver.
     - naive_solver.
@@ -264,13 +268,13 @@ Section cmra.
   Canonical Structure viewUR := Ucmra (view rel) view_ucmra_mixin.
 
   (** Operation *)
-  Lemma view_auth_frac_op p1 p2 a : ●V{p1 + p2} a ≡ ●V{p1} a ⋅ ●V{p2} a.
+  Lemma view_auth_frac_op dq1 dq2 a : ●V{dq1 ⋅ dq2} a ≡ ●V{dq1} a ⋅ ●V{dq2} a.
   Proof.
     intros; split; simpl; last by rewrite left_id.
     by rewrite -Some_op -pair_op agree_idemp.
   Qed.
-  Global Instance view_auth_frac_is_op q q1 q2 a :
-    IsOp q q1 q2 → IsOp' (●V{q} a) (●V{q1} a) (●V{q2} a).
+  Global Instance view_auth_frac_is_op dq dq1 dq2 a :
+    IsOp dq dq1 dq2 → IsOp' (●V{dq} a) (●V{dq1} a) (●V{dq2} a).
   Proof. rewrite /IsOp' /IsOp => ->. by rewrite -view_auth_frac_op. Qed.
 
   Lemma view_frag_op b1 b2 : â—¯V (b1 â‹… b2) = â—¯V b1 â‹… â—¯V b2.
@@ -302,31 +306,31 @@ Section cmra.
   Proof. apply (big_opMS_commute _). Qed.
 
   (** Validity *)
-  Lemma view_auth_frac_op_invN n p1 a1 p2 a2 :
-    ✓{n} (●V{p1} a1 ⋅ ●V{p2} a2) → a1 ≡{n}≡ a2.
+  Lemma view_auth_frac_op_invN n dq1 a1 dq2 a2 :
+    ✓{n} (●V{dq1} a1 ⋅ ●V{dq2} a2) → a1 ≡{n}≡ a2.
   Proof.
     rewrite /op /view_op_instance /= left_id -Some_op -pair_op view_validN_eq /=.
     intros (?&?& Eq &?). apply (inj to_agree), agree_op_invN. by rewrite Eq.
   Qed.
-  Lemma view_auth_frac_op_inv p1 a1 p2 a2 : ✓ (●V{p1} a1 ⋅ ●V{p2} a2) → a1 ≡ a2.
+  Lemma view_auth_frac_op_inv dq1 a1 dq2 a2 : ✓ (●V{dq1} a1 ⋅ ●V{dq2} a2) → a1 ≡ a2.
   Proof.
     intros ?. apply equiv_dist. intros n.
     by eapply view_auth_frac_op_invN, cmra_valid_validN.
   Qed.
-  Lemma view_auth_frac_op_inv_L `{!LeibnizEquiv A} p1 a1 p2 a2 :
-    ✓ (●V{p1} a1 ⋅ ●V{p2} a2) → a1 = a2.
+  Lemma view_auth_frac_op_inv_L `{!LeibnizEquiv A} dq1 a1 dq2 a2 :
+    ✓ (●V{dq1} a1 ⋅ ●V{dq2} 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) ↔ (q ≤ 1)%Qp ∧ rel n a ε.
+  Lemma view_auth_frac_validN n dq a : ✓{n} (●V{dq} a) ↔ ✓{n}dq ∧ 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. naive_solver. Qed.
+  Proof. rewrite view_auth_frac_validN. split; [naive_solver|done]. Qed.
 
-  Lemma view_auth_frac_op_validN n q1 q2 a1 a2 :
-    ✓{n} (●V{q1} a1 ⋅ ●V{q2} a2) ↔ (q1 + q2 ≤ 1)%Qp ∧ a1 ≡{n}≡ a2 ∧ rel n a1 ε.
+  Lemma view_auth_frac_op_validN n dq1 dq2 a1 a2 :
+    ✓{n} (●V{dq1} a1 ⋅ ●V{dq2} a2) ↔ ✓(dq1 ⋅ dq2) ∧ a1 ≡{n}≡ a2 ∧ rel n a1 ε.
   Proof.
     split.
     - intros Hval. assert (a1 ≡{n}≡ a2) as Ha by eauto using view_auth_frac_op_invN.
@@ -339,28 +343,28 @@ Section cmra.
   Lemma view_frag_validN n b : ✓{n} (◯V b) ↔ ∃ a, rel n a b.
   Proof. done. Qed.
 
-  Lemma view_both_frac_validN n q a b :
-    ✓{n} (●V{q} a ⋅ ◯V b) ↔ (q ≤ 1)%Qp ∧ rel n a b.
+  Lemma view_both_frac_validN n dq a b :
+    ✓{n} (●V{dq} a ⋅ ◯V b) ↔ ✓dq ∧ 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. naive_solver. Qed.
+  Proof. rewrite view_both_frac_validN. split; [naive_solver|done]. Qed.
 
-  Lemma view_auth_frac_valid q a : ✓ (●V{q} a) ↔ (q ≤ 1)%Qp ∧ ∀ n, rel n a ε.
+  Lemma view_auth_frac_valid dq a : ✓ (●V{dq} a) ↔ ✓dq ∧ ∀ 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. naive_solver. Qed.
+  Proof. rewrite view_auth_frac_valid. split; [naive_solver|done]. Qed.
 
-  Lemma view_auth_frac_op_valid q1 q2 a1 a2 :
-    ✓ (●V{q1} a1 ⋅ ●V{q2} a2) ↔ (q1 + q2 ≤ 1)%Qp ∧ a1 ≡ a2 ∧ ∀ n, rel n a1 ε.
+  Lemma view_auth_frac_op_valid dq1 dq2 a1 a2 :
+    ✓ (●V{dq1} a1 ⋅ ●V{dq2} a2) ↔ ✓(dq1 ⋅ dq2) ∧ a1 ≡ a2 ∧ ∀ n, rel n a1 ε.
   Proof.
-    rewrite !cmra_valid_validN equiv_dist. setoid_rewrite view_auth_frac_op_validN.
+    rewrite 1!cmra_valid_validN equiv_dist. setoid_rewrite view_auth_frac_op_validN.
     split; last naive_solver. intros Hv.
     split; last naive_solver. apply (Hv 0).
   Qed.
@@ -370,37 +374,37 @@ 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 ≤ 1)%Qp ∧ ∀ n, rel n a b.
+  Lemma view_both_frac_valid dq a b : ✓ (●V{dq} a ⋅ ◯V b) ↔ ✓dq ∧ ∀ 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. naive_solver. Qed.
+  Proof. rewrite view_both_frac_valid. split; [naive_solver|done]. Qed.
 
   (** Inclusion *)
-  Lemma view_auth_frac_includedN n p1 p2 a1 a2 b :
-    ●V{p1} a1 ≼{n} ●V{p2} a2 ⋅ ◯V b ↔ (p1 ≤ p2)%Qp ∧ a1 ≡{n}≡ a2.
+  Lemma view_auth_frac_includedN n dq1 dq2 a1 a2 b :
+    ●V{dq1} a1 ≼{n} ●V{dq2} a2 ⋅ ◯V b ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡{n}≡ a2.
   Proof.
     split.
     - intros [[[[qf agf]|] bf]
         [[?%(discrete_iff _ _) ?]%(inj Some) _]]; simplify_eq/=.
-      + split; [apply Qp_le_add_l|]. apply to_agree_includedN. by exists agf.
-      + split; [done|]. by apply (inj to_agree).
-    - intros [[[q ->]%frac_included| ->]%Qp_le_lteq ->].
+      + split; [left; apply cmra_included_l|]. apply to_agree_includedN. by exists agf.
+      + split; [right; done|]. by apply (inj to_agree).
+    - intros [[[? ->]| ->] ->].
       + rewrite view_auth_frac_op -assoc. apply cmra_includedN_l.
       + apply cmra_includedN_l.
   Qed.
-  Lemma view_auth_frac_included p1 p2 a1 a2 b :
-    ●V{p1} a1 ≼ ●V{p2} a2 ⋅ ◯V b ↔ (p1 ≤ p2)%Qp ∧ a1 ≡ a2.
+  Lemma view_auth_frac_included dq1 dq2 a1 a2 b :
+    ●V{dq1} a1 ≼ ●V{dq2} a2 ⋅ ◯V b ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡ a2.
   Proof.
     intros. split.
     - split.
       + by eapply (view_auth_frac_includedN 0), cmra_included_includedN.
       + apply equiv_dist=> n.
         by eapply view_auth_frac_includedN, cmra_included_includedN.
-    - intros [[[q ->]%frac_included| ->]%Qp_le_lteq ->].
+    - intros [[[dq ->]| ->] ->].
       + rewrite view_auth_frac_op -assoc. apply cmra_included_l.
       + apply cmra_included_l.
   Qed.
@@ -430,8 +434,9 @@ Section cmra.
 
   (** The weaker [view_both_included] lemmas below are a consequence of the
   [view_auth_included] and [view_frag_included] lemmas above. *)
-  Lemma view_both_frac_includedN n p1 p2 a1 a2 b1 b2 :
-    ●V{p1} a1 ⋅ ◯V b1 ≼{n} ●V{p2} a2 ⋅ ◯V b2 ↔ (p1 ≤ p2)%Qp ∧ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
+  Lemma view_both_frac_includedN n dq1 dq2 a1 a2 b1 b2 :
+    ●V{dq1} a1 ⋅ ◯V b1 ≼{n} ●V{dq2} a2 ⋅ ◯V b2 ↔
+      (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
   Proof.
     split.
     - intros. rewrite assoc. split.
@@ -440,8 +445,9 @@ Section cmra.
     - intros (?&->&?bf&->). rewrite (comm _ b1) view_frag_op assoc.
       by apply cmra_monoN_r, view_auth_frac_includedN.
   Qed.
-  Lemma view_both_frac_included p1 p2 a1 a2 b1 b2 :
-    ●V{p1} a1 ⋅ ◯V b1 ≼ ●V{p2} a2 ⋅ ◯V b2 ↔ (p1 ≤ p2)%Qp ∧ a1 ≡ a2 ∧ b1 ≼ b2.
+  Lemma view_both_frac_included dq1 dq2 a1 a2 b1 b2 :
+    ●V{dq1} a1 ⋅ ◯V b1 ≼ ●V{dq2} a2 ⋅ ◯V b2 ↔
+      (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡ a2 ∧ b1 ≼ b2.
   Proof.
     split.
     - intros. rewrite assoc. split.
@@ -462,7 +468,7 @@ Section cmra.
     (∀ n bf, rel n a (b ⋅ bf) → rel n a' (b' ⋅ bf)) →
     ●V a ⋅ ◯V b ~~> ●V a' ⋅ ◯V b'.
   Proof.
-    intros Hup; apply cmra_total_update=> n [[[q ag]|] bf] [/=].
+    intros Hup; apply cmra_total_update=> n [[[dq ag]|] bf] [/=].
     { by intros []%(exclusiveN_l _ _). }
     intros _ (a0 & <-%(inj to_agree) & Hrel). split; simpl; [done|].
     exists a'; split; [done|]. revert Hrel. rewrite !left_id. apply Hup.
@@ -490,16 +496,23 @@ Section cmra.
     intros Hup. rewrite -(right_id _ _ (●V a)) -(right_id _ _ (●V a')).
     apply view_update=> n bf. rewrite !left_id. apply Hup.
   Qed.
+  Lemma view_update_auth_persist dq a : ●V{dq} a ~~> ●V□ a.
+  Proof.
+    apply cmra_total_update.
+    move=> n [[[dq' ag]|] bf] [Hv ?]; last done. split; last done.
+    by apply (dfrac_discard_update dq _ (Some dq')).
+  Qed.
+
   Lemma view_update_frag b b' :
     (∀ a n bf, rel n a (b ⋅ bf) → rel n a (b' ⋅ bf)) →
     â—¯V b ~~> â—¯V b'.
   Proof.
-    rewrite !cmra_total_update view_validN_eq=> ? n [[[q ag]|] bf]; naive_solver.
+    rewrite !cmra_total_update view_validN_eq=> ? n [[[dq ag]|] bf]; naive_solver.
   Qed.
 
-  Lemma view_update_frac_alloc q a b :
+  Lemma view_update_frac_alloc dq a b :
     (∀ n bf, rel n a bf → rel n a (b ⋅ bf)) →
-    ●V{q} a ~~> ●V{q} a ⋅ ◯V b.
+    ●V{dq} a ~~> ●V{dq} a ⋅ ◯V b.
   Proof.
     intros Hup. apply cmra_total_update=> n [[[p ag]|] bf] [/=].
     - intros ? (a0 & Hag & Hrel). split; simpl; [done|].
@@ -512,18 +525,19 @@ Section cmra.
   Qed.
 
   Lemma view_local_update a b0 b1 a' b0' b1' :
-    (b0, b1) ~l~> (b0', b1') → 
+    (b0, b1) ~l~> (b0', b1') →
     (∀ n, view_rel_holds rel n a b0 → view_rel_holds rel n a' b0') →
     (●V a ⋅ ◯V b0, ●V a ⋅ ◯V b1) ~l~> (●V a' ⋅ ◯V b0', ●V a' ⋅ ◯V b1').
   Proof.
     rewrite !local_update_unital.
-    move=> Hup Hrel n [[[q ag]|] bf] /view_both_validN Hrel' [/=].
-    - rewrite right_id -Some_op -pair_op frac_op=> /Some_dist_inj [/= H1q _].
-      by destruct (Qp_add_id_free 1 q).
+    move=> Hup Hrel n [[[qd ag]|] bf] /view_both_validN Hrel' [/=].
+    - rewrite right_id -Some_op -pair_op => /Some_dist_inj [/= H1q _].
+      by destruct (id_free_r (DfracOwn 1) qd).
     - rewrite !left_id=> _ Hb0.
       destruct (Hup n bf) as [? Hb0']; [by eauto using view_rel_validN..|].
       split; [apply view_both_validN; by auto|]. by rewrite -assoc Hb0'.
   Qed.
+
 End cmra.
 
 (** * Utilities to construct functors *)
@@ -592,6 +606,6 @@ Proof.
     by rewrite -agree_map_to_agree -Hag.
   - intros [o bf]. apply Some_proper; rewrite /view_map /=.
     f_equiv; by rewrite cmra_morphism_core.
-  - intros [[[p1 ag1]|] bf1] [[[p2 ag2]|] bf2];
+  - intros [[[dq1 ag1]|] bf1] [[[dq2 ag2]|] bf2];
       try apply View_proper=> //=; by rewrite cmra_morphism_op.
 Qed.
diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index 8d943d4ff146bd8b114b2508fe2d5444e4c76a72..a544ba591bc369ab78700c2a1c3d81b1ba17fd41 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -145,23 +145,23 @@ Section view.
   Implicit Types b : B.
   Implicit Types x y : view rel.
 
-  Lemma view_both_frac_validI_1 (relI : uPred M) q a b :
+  Lemma view_both_frac_validI_1 (relI : uPred M) dq a b :
     (∀ n (x : M), rel n a b → relI n x) →
-    ✓ (●V{q} a ⋅ ◯V b : view rel) ⊢ ⌜q ≤ 1⌝%Qp ∧ relI.
+    ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊢ ⌜✓dq⌝ ∧ 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 :
+  Lemma view_both_frac_validI_2 (relI : uPred M) dq a b :
     (∀ n (x : M), relI n x → rel n a b) →
-    ⌜q ≤ 1⌝%Qp ∧ relI ⊢ ✓ (●V{q} a ⋅ ◯V b : view rel).
+    ⌜✓dq⌝%Qp ∧ relI ⊢ ✓ (●V{dq} 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 :
+  Lemma view_both_frac_validI (relI : uPred M) dq a b :
     (∀ n (x : M), rel n a b ↔ relI n x) →
-    ✓ (●V{q} a ⋅ ◯V b : view rel) ⊣⊢ ⌜q ≤ 1⌝%Qp ∧ relI.
+    ✓ (●V{dq} a ⋅ ◯V b : view rel) ⊣⊢ ⌜✓dq⌝ ∧ relI.
   Proof.
     intros. apply (anti_symm _);
       [apply view_both_frac_validI_1|apply view_both_frac_validI_2]; naive_solver.
@@ -186,11 +186,11 @@ Section view.
       [apply view_both_validI_1|apply view_both_validI_2]; naive_solver.
   Qed.
 
-  Lemma view_auth_frac_validI (relI : uPred M) q a :
+  Lemma view_auth_frac_validI (relI : uPred M) dq a :
     (∀ n (x : M), relI n x ↔ rel n a ε) →
-    ✓ (●V{q} a : view rel) ⊣⊢ ⌜q ≤ 1⌝%Qp ∧ relI.
+    ✓ (●V{dq} a : view rel) ⊣⊢ ⌜✓dq⌝ ∧ relI.
   Proof.
-    intros. rewrite -(right_id ε op (●V{q} a)). by apply view_both_frac_validI.
+    intros. rewrite -(right_id ε op (●V{dq} a)). by apply view_both_frac_validI.
   Qed.
   Lemma view_auth_validI (relI : uPred M) a :
     (∀ n (x : M), relI n x ↔ rel n a ε) →
@@ -208,7 +208,7 @@ Section auth.
   Implicit Types a b : A.
   Implicit Types x y : auth A.
 
-  Lemma auth_auth_frac_validI q a : ✓ (●{q} a) ⊣⊢ ⌜q ≤ 1⌝%Qp ∧ ✓ a.
+  Lemma auth_auth_frac_validI dq a : ✓ (●{dq} a) ⊣⊢ ⌜✓dq⌝ ∧ ✓ a.
   Proof.
     apply view_auth_frac_validI=> n. uPred.unseal; split; [|by intros [??]].
     split; [|done]. apply ucmra_unit_leastN.
@@ -224,8 +224,8 @@ Section auth.
     rewrite auth_view_rel_exists. by uPred.unseal.
   Qed.
 
-  Lemma auth_both_frac_validI q a b :
-    ✓ (●{q} a ⋅ ◯ b) ⊣⊢ ⌜q ≤ 1⌝%Qp ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
+  Lemma auth_both_frac_validI dq a b :
+    ✓ (●{dq} a ⋅ ◯ b) ⊣⊢ ⌜✓dq⌝ ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
   Proof. apply view_both_frac_validI=> n. by uPred.unseal. Qed.
   Lemma auth_both_validI a b :
     ✓ (● a ⋅ ◯ b) ⊣⊢ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
diff --git a/iris/base_logic/lib/gset_bij.v b/iris/base_logic/lib/gset_bij.v
index 1144bf6f500b384428a6585a7c1fd4593c6cc0fa..63c7d346be18476521771be8e87d3d7f2a90f7ed 100644
--- a/iris/base_logic/lib/gset_bij.v
+++ b/iris/base_logic/lib/gset_bij.v
@@ -38,8 +38,8 @@ Global Instance subG_gset_bijΣ `{Countable A, Countable B} Σ :
 Proof. solve_inG. Qed.
 
 Definition gset_bij_own_auth_def `{gset_bijG Σ A B} (γ : gname)
-    (q : Qp) (L : gset (A * B)) : iProp Σ :=
-  own γ (gset_bij_auth q L).
+    (dq : dfrac) (L : gset (A * B)) : iProp Σ :=
+  own γ (gset_bij_auth dq L).
 Definition gset_bij_own_auth_aux : seal (@gset_bij_own_auth_def). Proof. by eexists. Qed.
 Definition gset_bij_own_auth := unseal gset_bij_own_auth_aux.
 Definition gset_bij_own_auth_eq :
@@ -69,23 +69,23 @@ Section gset_bij.
   Proof. rewrite gset_bij_own_elem_eq. apply _. Qed.
 
   Global Instance gset_bij_own_auth_fractional γ L :
-    Fractional (λ q, gset_bij_own_auth γ q L).
+    Fractional (λ q, gset_bij_own_auth γ (DfracOwn q) L).
   Proof.
     intros p q. rewrite gset_bij_own_auth_eq -own_op gset_bij_auth_frac_op //.
   Qed.
   Global Instance gset_bij_own_auth_as_fractional γ q L :
-    AsFractional (gset_bij_own_auth γ q L) (λ q, gset_bij_own_auth γ q L) q.
+    AsFractional (gset_bij_own_auth γ (DfracOwn q) L) (λ q, gset_bij_own_auth γ (DfracOwn q) L) q.
   Proof. split; [auto|apply _]. Qed.
 
-  Lemma gset_bij_own_auth_agree γ q1 q2 L1 L2 :
-    gset_bij_own_auth γ q1 L1 -∗ gset_bij_own_auth γ q2 L2 -∗
-    ⌜✓ (q1 + q2)%Qp ∧ L1 = L2 ∧ gset_bijective L1⌝.
+  Lemma gset_bij_own_auth_agree γ dq1 dq2 L1 L2 :
+    gset_bij_own_auth γ dq1 L1 -∗ gset_bij_own_auth γ dq2 L2 -∗
+    ⌜✓ (dq1 ⋅ dq2) ∧ L1 = L2 ∧ gset_bijective L1⌝.
   Proof.
     rewrite gset_bij_own_auth_eq. iIntros "H1 H2".
     by iDestruct (own_valid_2 with "H1 H2") as %?%gset_bij_auth_frac_op_valid.
   Qed.
   Lemma gset_bij_own_auth_exclusive γ L1 L2 :
-    gset_bij_own_auth γ 1 L1 -∗ gset_bij_own_auth γ 1 L2 -∗ False.
+    gset_bij_own_auth γ (DfracOwn 1) L1 -∗ gset_bij_own_auth γ (DfracOwn 1) L2 -∗ False.
   Proof.
     iIntros "H1 H2".
     by iDestruct (gset_bij_own_auth_agree with "H1 H2") as %[[] _].
@@ -122,24 +122,24 @@ Section gset_bij.
 
   Lemma gset_bij_own_alloc L :
     gset_bijective L →
-    ⊢ |==> ∃ γ, gset_bij_own_auth γ 1 L ∗ [∗ set] ab ∈ L, gset_bij_own_elem γ ab.1 ab.2.
+    ⊢ |==> ∃ γ, gset_bij_own_auth γ (DfracOwn 1) L ∗ [∗ set] ab ∈ L, gset_bij_own_elem γ ab.1 ab.2.
   Proof.
-    intro. iAssert (∃ γ, gset_bij_own_auth γ 1 L)%I with "[>]" as (γ) "Hauth".
+    intro. iAssert (∃ γ, gset_bij_own_auth γ (DfracOwn 1) L)%I with "[>]" as (γ) "Hauth".
     { rewrite gset_bij_own_auth_eq. iApply own_alloc. by apply gset_bij_auth_valid. }
     iExists γ. iModIntro. iSplit; [done|].
     by iApply gset_bij_own_elem_get_big.
   Qed.
   Lemma gset_bij_own_alloc_empty :
-    ⊢ |==> ∃ γ, gset_bij_own_auth γ 1 (∅ : gset (A * B)).
+    ⊢ |==> ∃ γ, gset_bij_own_auth γ (DfracOwn 1) (∅ : gset (A * B)).
   Proof. iMod (gset_bij_own_alloc ∅) as (γ) "[Hauth _]"; by auto. Qed.
 
   Lemma gset_bij_own_extend {γ L} a b :
     (∀ b', (a, b') ∉ L) → (∀ a', (a', b) ∉ L) →
-    gset_bij_own_auth γ 1 L ==∗
-    gset_bij_own_auth γ 1 ({[(a, b)]} ∪ L) ∗ gset_bij_own_elem γ a b.
+    gset_bij_own_auth γ (DfracOwn 1) L ==∗
+    gset_bij_own_auth γ (DfracOwn 1) ({[(a, b)]} ∪ L) ∗ gset_bij_own_elem γ a b.
   Proof.
     iIntros (??) "Hauth".
-    iAssert (gset_bij_own_auth γ 1 ({[a, b]} ∪ L)) with "[> Hauth]" as "Hauth".
+    iAssert (gset_bij_own_auth γ (DfracOwn 1) ({[a, b]} ∪ L)) with "[> Hauth]" as "Hauth".
     { rewrite gset_bij_own_auth_eq. iApply (own_update with "Hauth").
       by apply gset_bij_auth_extend. }
     iModIntro. iSplit; [done|].
@@ -149,8 +149,8 @@ Section gset_bij.
   Lemma gset_bij_own_extend_internal {γ L} a b :
     (∀ b', gset_bij_own_elem γ a b' -∗ False) -∗
     (∀ a', gset_bij_own_elem γ a' b -∗ False) -∗
-    gset_bij_own_auth γ 1 L ==∗
-    gset_bij_own_auth γ 1 ({[(a, b)]} ∪ L) ∗ gset_bij_own_elem γ a b.
+    gset_bij_own_auth γ (DfracOwn 1) L ==∗
+    gset_bij_own_auth γ (DfracOwn 1) ({[(a, b)]} ∪ L) ∗ gset_bij_own_elem γ a b.
   Proof.
     iIntros "Ha Hb HL".
     iAssert ⌜∀ b', (a, b') ∉ L⌝%I as %?.