diff --git a/CHANGELOG.md b/CHANGELOG.md
index ac2d07301e3b3550dfbd6c8ee26b7a599acf216a..dc605ae0eef83407c954bf9064a7f22df1f169c9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -23,6 +23,14 @@ lemma.
 * Remove `view_auth_frac_op`, `auth_auth_frac_op`, `gmap_view_auth_frac_op`; the
   corresponding `dfrac` lemmas can be used instead (together with `dfrac_op_own`
   if needed).
+* Equip `mono_nat` algebra with support for `dfrac`, make API more consistent,
+  and add notation for algebra elements. See `iris/algebra/lib/mono_nat.v` for
+  details. This affects some existing terms and lemmas:
+  - `mono_nat_auth` now takes a `dfrac`, but the recommendation is to port to the notation.
+  - `mono_nat_lb_op`: direction of equality is swapped.
+  - `mono_nat_auth_frac_op`, `mono_nat_auth_frac_op_valid`,
+    `mono_nat_auth_frac_valid`, `mono_nat_both_frac_valid`: use `dfrac` variant
+    instead.
 
 **Changes in `bi`:**
 
diff --git a/iris/algebra/lib/mono_nat.v b/iris/algebra/lib/mono_nat.v
index 7c5fe7e4fb629d67ab214d1bf33a9464b756642e..b712ad6e87424d14e6b76cc6dc28d553b9360378 100644
--- a/iris/algebra/lib/mono_nat.v
+++ b/iris/algebra/lib/mono_nat.v
@@ -11,32 +11,42 @@ Definition mono_natUR := authUR max_natUR.
 
 (** [mono_nat_auth] is the authoritative element. The definition includes the
 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
+[mono_nat_lb n ≼ mono_nat_auth dq n], does not require a frame-preserving
 update. *)
-Definition mono_nat_auth (q : Qp) (n : nat) : mono_nat :=
-  ●{#q} MaxNat n ⋅ ◯ MaxNat n.
+Definition mono_nat_auth (dq : dfrac) (n : nat) : mono_nat :=
+  ●{dq} MaxNat n ⋅ ◯ MaxNat n.
 Definition mono_nat_lb (n : nat) : mono_nat := â—¯ MaxNat n.
 
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
+Notation "●MN{ dq } a" :=
+  (mono_nat_auth dq a) (at level 20, format "●MN{ dq }  a").
+Notation "●MN{# q } a" :=
+  (mono_nat_auth (DfracOwn q) a) (at level 20, format "●MN{# q }  a").
+Notation "●MN□ a" := (mono_nat_auth DfracDiscarded a) (at level 20, format "●MN□  a").
+Notation "●MN a" := (mono_nat_auth (DfracOwn 1) a) (at level 20).
+Notation "â—¯MN a" := (mono_nat_lb a) (at level 20).
+
 Section mono_nat.
   Implicit Types (n : nat).
 
-  Global Instance mono_nat_lb_core_id n : CoreId (mono_nat_lb n).
+  Global Instance mono_nat_lb_core_id n : CoreId (â—¯MN n).
   Proof. apply _. Qed.
 
-  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.
+  Lemma mono_nat_auth_dfrac_op dq1 dq2 n :
+    ●MN{dq1 ⋅ dq2} n ≡ ●MN{dq1} n ⋅ ●MN{dq2} n.
   Proof.
-    rewrite /mono_nat_auth -dfrac_op_own auth_auth_dfrac_op.
-    rewrite (comm _ (●{#q2} _)) -!assoc (assoc _ (◯ _)).
+    rewrite /mono_nat_auth auth_auth_dfrac_op.
+    rewrite (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
     by rewrite -core_id_dup (comm _ (â—¯ _)).
   Qed.
 
   Lemma mono_nat_lb_op n1 n2 :
-    mono_nat_lb n1 â‹… mono_nat_lb n2 = mono_nat_lb (n1 `max` n2).
+    â—¯MN (n1 `max` n2) = â—¯MN n1 â‹… â—¯MN n2.
   Proof. rewrite -auth_frag_op max_nat_op //. Qed.
 
-  Lemma mono_nat_auth_lb_op q n :
-    mono_nat_auth q n ≡ mono_nat_auth q n ⋅ mono_nat_lb n.
+  Lemma mono_nat_auth_lb_op dq n :
+    ●MN{dq} n ≡ ●MN{dq} n ⋅ ◯MN n.
   Proof.
     rewrite /mono_nat_auth /mono_nat_lb.
     rewrite -!assoc -auth_frag_op max_nat_op.
@@ -47,53 +57,60 @@ Section mono_nat.
   smaller lower-bound *)
   Lemma mono_nat_lb_op_le_l n n' :
     n' ≤ n →
-    mono_nat_lb n = mono_nat_lb n' â‹… mono_nat_lb n.
-  Proof. intros. rewrite mono_nat_lb_op Nat.max_r //. Qed.
+    â—¯MN n = â—¯MN n' â‹… â—¯MN n.
+  Proof. intros. rewrite -mono_nat_lb_op Nat.max_r //. Qed.
 
-  Lemma mono_nat_auth_frac_valid q n : ✓ mono_nat_auth q n ↔ (q ≤ 1)%Qp.
+  Lemma mono_nat_auth_dfrac_valid dq n : (✓ ●MN{dq} n) ↔ ✓ dq.
   Proof.
     rewrite /mono_nat_auth auth_both_dfrac_valid_discrete /=. naive_solver.
   Qed.
-  Lemma mono_nat_auth_valid n : ✓ mono_nat_auth 1 n.
+  Lemma mono_nat_auth_valid n : ✓ ●MN n.
   Proof. by apply auth_both_valid. Qed.
 
-  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.
+  Lemma mono_nat_auth_dfrac_op_valid dq1 dq2 n1 n2 :
+    ✓ (●MN{dq1} n1 ⋅ ●MN{dq2} n2) ↔ ✓ (dq1 ⋅ dq2) ∧ n1 = n2.
   Proof.
-    rewrite /mono_nat_auth (comm _ (●{#q2} _)) -!assoc (assoc _ (◯ _)).
+    rewrite /mono_nat_auth (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
     rewrite -auth_frag_op (comm _ (â—¯ _)) assoc. split.
     - move=> /cmra_valid_op_l /auth_auth_dfrac_op_valid. naive_solver.
     - intros [? ->]. rewrite -core_id_dup -auth_auth_dfrac_op.
       by apply auth_both_dfrac_valid_discrete.
   Qed.
   Lemma mono_nat_auth_op_valid n1 n2 :
-    ✓ (mono_nat_auth 1 n1 ⋅ mono_nat_auth 1 n2) ↔ False.
-  Proof. rewrite mono_nat_auth_frac_op_valid. naive_solver. Qed.
+    ✓ (●MN n1 ⋅ ●MN n2) ↔ False.
+  Proof. rewrite mono_nat_auth_dfrac_op_valid. naive_solver. Qed.
 
-  Lemma mono_nat_both_frac_valid q n m :
-    ✓ (mono_nat_auth q n ⋅ mono_nat_lb m) ↔ (q ≤ 1)%Qp ∧ m ≤ n.
+  Lemma mono_nat_both_dfrac_valid dq n m :
+    ✓ (●MN{dq} n ⋅ ◯MN m) ↔ ✓ dq ∧ m ≤ n.
   Proof.
     rewrite /mono_nat_auth /mono_nat_lb -assoc -auth_frag_op.
     rewrite auth_both_dfrac_valid_discrete max_nat_included /=.
     naive_solver lia.
   Qed.
   Lemma mono_nat_both_valid n m :
-    ✓ (mono_nat_auth 1 n ⋅ mono_nat_lb m) ↔ m ≤ n.
-  Proof. rewrite mono_nat_both_frac_valid. naive_solver. Qed.
+    ✓ (●MN n ⋅ ◯MN m) ↔ m ≤ n.
+  Proof. rewrite mono_nat_both_dfrac_valid dfrac_valid_own. naive_solver. Qed.
 
-  Lemma mono_nat_lb_mono n1 n2 : n1 ≤ n2 → mono_nat_lb n1 ≼ mono_nat_lb n2.
+  Lemma mono_nat_lb_mono n1 n2 : n1 ≤ n2 → ◯MN n1 ≼ ◯MN n2.
   Proof. intros. by apply auth_frag_mono, max_nat_included. Qed.
 
-  Lemma mono_nat_included q n : mono_nat_lb n ≼ mono_nat_auth q n.
+  Lemma mono_nat_included dq n : ◯MN n ≼ ●MN{dq} n.
   Proof. apply cmra_included_r. Qed.
 
   Lemma mono_nat_update {n} n' :
-    n ≤ n' →
-    mono_nat_auth 1 n ~~> mono_nat_auth 1 n'.
+    n ≤ n' → ●MN n ~~> ●MN n'.
   Proof.
     intros. rewrite /mono_nat_auth /mono_nat_lb.
     by apply auth_update, max_nat_local_update.
   Qed.
+
+  Lemma mono_nat_auth_persist n dq :
+    ●MN{dq} n ~~> ●MN□ n.
+  Proof.
+    intros. rewrite /mono_nat_auth /mono_nat_lb.
+    eapply cmra_update_op_proper; last done.
+    eapply auth_update_auth_persist.
+  Qed.
 End mono_nat.
 
 Typeclasses Opaque mono_nat_auth mono_nat_lb.
diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index e3794680c39796c912d9bc7faea69be45ad2d54d..99389ea1d11c82650061c9a2e39cca5eae6eb45b 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -21,7 +21,7 @@ Proof. solve_inG. Qed.
 
 Definition mono_nat_auth_own_def `{!mono_natG Σ}
     (γ : gname) (q : Qp) (n : nat) : iProp Σ :=
-  own γ (mono_nat_auth q n).
+  own γ (●MN{#q} n).
 Definition mono_nat_auth_own_aux : seal (@mono_nat_auth_own_def). Proof. by eexists. Qed.
 Definition mono_nat_auth_own := mono_nat_auth_own_aux.(unseal).
 Definition mono_nat_auth_own_eq :
@@ -29,7 +29,7 @@ Definition mono_nat_auth_own_eq :
 Global Arguments mono_nat_auth_own {Σ _} γ q n.
 
 Definition mono_nat_lb_own_def `{!mono_natG Σ} (γ : gname) (n : nat): iProp Σ :=
-  own γ (mono_nat_lb n).
+  own γ (◯MN n).
 Definition mono_nat_lb_own_aux : seal (@mono_nat_lb_own_def). Proof. by eexists. Qed.
 Definition mono_nat_lb_own := mono_nat_lb_own_aux.(unseal).
 Definition mono_nat_lb_own_eq :
@@ -53,7 +53,7 @@ Section mono_nat.
 
   Global Instance mono_nat_auth_own_fractional γ n :
     Fractional (λ q, mono_nat_auth_own γ q n).
-  Proof. unseal. intros p q. rewrite -own_op mono_nat_auth_frac_op //. Qed.
+  Proof. unseal. intros p q. rewrite -own_op -mono_nat_auth_dfrac_op //. Qed.
   Global Instance mono_nat_auth_own_as_fractional γ q n :
     AsFractional (mono_nat_auth_own γ q n) (λ q, mono_nat_auth_own γ q n) q.
   Proof. split; [auto|apply _]. Qed.
@@ -64,7 +64,7 @@ Section mono_nat.
     ⌜(q1 + q2 ≤ 1)%Qp ∧ n1 = n2⌝.
   Proof.
     unseal. iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %?%mono_nat_auth_frac_op_valid; done.
+    iDestruct (own_valid_2 with "H1 H2") as %?%mono_nat_auth_dfrac_op_valid; done.
   Qed.
   Lemma mono_nat_auth_own_exclusive γ n1 n2 :
     mono_nat_auth_own γ 1 n1 -∗ mono_nat_auth_own γ 1 n2 -∗ False.
@@ -77,7 +77,7 @@ Section mono_nat.
     mono_nat_auth_own γ q n -∗ mono_nat_lb_own γ m -∗ ⌜(q ≤ 1)%Qp ∧ m ≤ n⌝.
   Proof.
     unseal. iIntros "Hauth Hlb".
-    iDestruct (own_valid_2 with "Hauth Hlb") as %Hvalid%mono_nat_both_frac_valid.
+    iDestruct (own_valid_2 with "Hauth Hlb") as %Hvalid%mono_nat_both_dfrac_valid.
     auto.
   Qed.
 
@@ -97,7 +97,7 @@ Section mono_nat.
   Lemma mono_nat_own_alloc n :
     ⊢ |==> ∃ γ, mono_nat_auth_own γ 1 n ∗ mono_nat_lb_own γ n.
   Proof.
-    unseal. iMod (own_alloc (mono_nat_auth 1 n ⋅ mono_nat_lb n)) as (γ) "[??]".
+    unseal. iMod (own_alloc (●MN n ⋅ ◯MN n)) as (γ) "[??]".
     { apply mono_nat_both_valid; auto. }
     auto with iFrame.
   Qed.