diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index ec5d2b9bfa3bd7a72b961eb1cd9e9d73a663a518..3a1bcc81c71513d0cd992e4d47f21f372188a070 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -150,7 +150,7 @@ Proof.
   naive_solver eauto using cmra_validN_includedN.
 Qed.
 
-Lemma auth_frag_validN n a : ✓{n} a ↔ ✓{n} (◯ a).
+Lemma auth_frag_validN n a : ✓{n} (◯ a) ↔ ✓{n} a.
 Proof. done. Qed.
 Lemma auth_auth_frac_validN n q a :
   ✓{n} (●{q} a) ↔ ✓{n} q ∧ ✓{n} a.
@@ -176,26 +176,29 @@ Proof.
   rewrite auth_both_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
 Qed.
 
-Lemma auth_frag_valid a : ✓ a ↔ ✓ (◯ a).
+Lemma auth_frag_valid a : ✓ (◯ a) ↔ ✓ a.
 Proof. done. Qed.
-Lemma auth_auth_frac_valid q a : ✓ q ∧ ✓ a ↔ ✓ (●{q} a).
+Lemma auth_auth_frac_valid q a : ✓ (●{q} a) ↔ ✓ q ∧ ✓ a.
 Proof.
   rewrite auth_valid_eq /=. apply and_iff_compat_l. split.
-  - intros. exists a. split; [done|].
-    split; by [apply ucmra_unit_leastN|apply cmra_valid_validN].
   - intros H'. apply cmra_valid_validN. intros n.
     by destruct (H' n) as [? [->%to_agree_injN [??]]].
+  - intros. exists a. split; [done|].
+    split; by [apply ucmra_unit_leastN|apply cmra_valid_validN].
 Qed.
-Lemma auth_auth_valid a : ✓ a ↔ ✓ (● a).
-Proof. rewrite -auth_auth_frac_valid frac_valid'. naive_solver. Qed.
-Lemma auth_both_frac_valid q a b : ✓ q → ✓ a → b ≼ a → ✓ (●{q} a ⋅ ◯ b).
+Lemma auth_auth_valid a : ✓ (● a) ↔ ✓ a.
+Proof. rewrite auth_auth_frac_valid 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).
 Proof.
   intros Val1 Val2 Incl. rewrite auth_valid_eq /=. split; [done|].
   intros n. exists a. split; [done|]. rewrite left_id.
   split; by [apply cmra_included_includedN|apply cmra_valid_validN].
 Qed.
-Lemma auth_both_valid a b : ✓ a → b ≼ a → ✓ (● a ⋅ ◯ b).
-Proof. intros ??. by apply auth_both_frac_valid. Qed.
+Lemma auth_both_valid_2 a b : ✓ a → b ≼ a → ✓ (● a ⋅ ◯ b).
+Proof. intros ??. by apply auth_both_frac_valid_2. Qed.
 
 Lemma auth_valid_discrete `{!CmraDiscrete A} x :
   ✓ x ↔ match auth_auth_proj x with
@@ -208,7 +211,7 @@ Proof.
   setoid_rewrite <-(discrete_iff _ a).
   setoid_rewrite <-cmra_discrete_valid_iff. naive_solver eauto using O.
 Qed.
-Lemma auth_frac_valid_discrete_2 `{!CmraDiscrete A} q a b :
+Lemma auth_both_frac_valid `{!CmraDiscrete A} q a b :
   ✓ (●{q} a ⋅ ◯ b) ↔ ✓ q ∧ b ≼ a ∧ ✓ a.
 Proof.
   rewrite auth_valid_discrete /=. apply and_iff_compat_l.
@@ -216,8 +219,8 @@ Proof.
   - by intros [?[->%to_agree_inj]].
   - naive_solver.
 Qed.
-Lemma auth_valid_discrete_2 `{!CmraDiscrete A} a b : ✓ (● a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
-Proof. rewrite auth_frac_valid_discrete_2 frac_valid'. naive_solver. Qed.
+Lemma auth_both_valid `{!CmraDiscrete A} a b : ✓ (● a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
+Proof. rewrite auth_both_frac_valid frac_valid'. naive_solver. Qed.
 
 Lemma auth_cmra_mixin : CmraMixin (auth A).
 Proof.
@@ -293,7 +296,7 @@ Proof. by rewrite /op /auth_op /= left_id. Qed.
 Lemma auth_both_op a b : Auth (Some (1%Qp,to_agree a)) b ≡ ● a ⋅ ◯ b.
 Proof. by rewrite auth_both_frac_op. Qed.
 
-Lemma auth_auth_frac_op p q a: ●{p} a ⋅ ●{q} a ≡ ●{p + q} a.
+Lemma auth_auth_frac_op p q a : ●{p + q} a ≡ ●{p} a ⋅ ●{q} a.
 Proof.
   intros; split; simpl; last by rewrite left_id.
   by rewrite -Some_op pair_op agree_idemp.
diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v
index 0706fe627a43af9fecdd99b5b0b5d0ff2b6a597d..3124b47691239f50e77973cd44d41e12ab0d3dff 100644
--- a/theories/algebra/frac_auth.v
+++ b/theories/algebra/frac_auth.v
@@ -49,7 +49,7 @@ Section frac_auth.
   Lemma frac_auth_validN n a : ✓{n} a → ✓{n} (●! a ⋅ ◯! a).
   Proof. by rewrite auth_both_validN. Qed.
   Lemma frac_auth_valid a : ✓ a → ✓ (●! a ⋅ ◯! a).
-  Proof. intros. by apply auth_both_valid. Qed.
+  Proof. intros. by apply auth_both_valid_2. Qed.
 
   Lemma frac_auth_agreeN n a b : ✓{n} (●! a ⋅ ◯! b) → a ≡{n}≡ b.
   Proof.
@@ -67,7 +67,7 @@ Section frac_auth.
   Proof. by rewrite auth_both_validN /= => -[/Some_pair_includedN [_ ?] _]. Qed.
   Lemma frac_auth_included `{CmraDiscrete A} q a b :
     ✓ (●! a ⋅ ◯!{q} b) → Some b ≼ Some a.
-  Proof. by rewrite auth_valid_discrete_2 /= => -[/Some_pair_included [_ ?] _]. Qed.
+  Proof. by rewrite auth_both_valid /= => -[/Some_pair_included [_ ?] _]. Qed.
   Lemma frac_auth_includedN_total `{CmraTotal A} n q a b :
     ✓{n} (●! a ⋅ ◯!{q} b) → b ≼{n} a.
   Proof. intros. by eapply Some_includedN_total, frac_auth_includedN. Qed.
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index 2a6974c29769c2dd8cb88b772108023dbd59d805..c5a8b494a3e540ae9e5ee66c339da83fc6571ad4 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -108,7 +108,7 @@ Section auth.
   Proof.
     iIntros (??) "Hφ". rewrite /auth_own /auth_ctx.
     iMod (own_alloc_strong (● f t ⋅ ◯ f t) I) as (γ) "[% [Hγ Hγ']]";
-      [done|by apply auth_valid_discrete_2|].
+      [done|by apply auth_both_valid|].
     iMod (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']") as "#?".
     { iNext. rewrite /auth_inv. iExists t. by iFrame. }
     eauto.
@@ -140,7 +140,7 @@ Section auth.
     iIntros "[Hinv Hγf]". rewrite /auth_inv /auth_own.
     iDestruct "Hinv" as (t) "[>Hγa Hφ]".
     iModIntro. iExists t.
-    iDestruct (own_valid_2 with "Hγa Hγf") as % [? ?]%auth_valid_discrete_2.
+    iDestruct (own_valid_2 with "Hγa Hγf") as % [? ?]%auth_both_valid.
     iSplit; first done. iFrame. iIntros (u b) "[% Hφ]".
     iMod (own_update_2 with "Hγa Hγf") as "[Hγa Hγf]".
     { eapply auth_update; eassumption. }
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 597c05835f1bd95bfd75fcb68c5360f9d89316ca..600b2ad191f6afbad0626db89af71faa5e87d2eb 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -78,7 +78,7 @@ Lemma box_own_auth_agree γ b1 b2 :
   box_own_auth γ (● Excl' b1) ∗ box_own_auth γ (◯ Excl' b2) ⊢ ⌜b1 = b2⌝.
 Proof.
   rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
-  by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete_2.
+  by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_both_valid.
 Qed.
 
 Lemma box_own_auth_update γ b1 b2 b3 :
@@ -110,7 +110,7 @@ Proof.
   iDestruct 1 as (Φ) "[#HeqP Hf]".
   iMod (own_alloc_cofinite (● Excl' false ⋅ ◯ Excl' false,
     Some (to_agree (Next (iProp_unfold Q)))) (dom _ f))
-    as (γ) "[Hdom Hγ]"; first by (split; [apply auth_valid_discrete_2|]).
+    as (γ) "[Hdom Hγ]"; first by (split; [apply auth_both_valid|]).
   rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
   iDestruct "Hdom" as % ?%not_elem_of_dom.
   iMod (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv".
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index cb0b414a240dad85c02ebeeab93c04dfe90e29f8..13502ff5e410e602edceb142de41d54e7db804c8 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -76,7 +76,7 @@ Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
   (|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
 Proof.
   iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
-  { rewrite -auth_auth_valid. exact: to_gen_heap_valid. }
+  { rewrite auth_auth_valid. exact: to_gen_heap_valid. }
   iModIntro. by iExists (GenHeapG L V Σ _ _ _ γ).
 Qed.
 
@@ -105,7 +105,7 @@ Section gen_heap.
   Proof.
     apply wand_intro_r.
     rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op own_valid discrete_valid.
-    f_equiv. rewrite -auth_frag_valid op_singleton singleton_valid pair_op.
+    f_equiv. rewrite auth_frag_valid op_singleton singleton_valid pair_op.
     by intros [_ ?%agree_op_invL'].
   Qed.
 
@@ -154,7 +154,7 @@ Section gen_heap.
   Proof.
     iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
     iDestruct (own_valid_2 with "Hσ Hl")
-      as %[Hl%gen_heap_singleton_included _]%auth_valid_discrete_2; auto.
+      as %[Hl%gen_heap_singleton_included _]%auth_both_valid; auto.
   Qed.
 
   Lemma gen_heap_update σ l v1 v2 :
@@ -162,7 +162,7 @@ Section gen_heap.
   Proof.
     iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
     iDestruct (own_valid_2 with "Hσ Hl")
-      as %[Hl%gen_heap_singleton_included _]%auth_valid_discrete_2.
+      as %[Hl%gen_heap_singleton_included _]%auth_both_valid.
     iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
     { eapply auth_update, singleton_local_update,
         (exclusive_local_update _ (1%Qp, to_agree (v2:leibnizC _)))=> //.
diff --git a/theories/base_logic/lib/proph_map.v b/theories/base_logic/lib/proph_map.v
index 939ee30596e8547d80383b4cc1e98fa7cb82f7de..c1a990384621114d74c1e283ae2aea2556103828 100644
--- a/theories/base_logic/lib/proph_map.v
+++ b/theories/base_logic/lib/proph_map.v
@@ -111,7 +111,7 @@ Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
   (|==> ∃ _ : proph_mapG P V PVS, proph_map_ctx pvs ps)%I.
 Proof.
   iMod (own_alloc (● to_proph_map ∅)) as (γ) "Hh".
-  { rewrite -auth_auth_valid. exact: to_proph_map_valid. }
+  { rewrite auth_auth_valid. exact: to_proph_map_valid. }
   iModIntro. iExists (ProphMapG P V PVS _ _ _ γ), ∅. iSplit; last by iFrame.
   iPureIntro. split =>//.
 Qed.
@@ -153,7 +153,7 @@ Section proph_map.
   Proof.
     iIntros "[HR Hp]". iDestruct "HR" as (R) "[HP H●]". iDestruct "HP" as %[Hres Hdom].
     rewrite /proph_map_ctx proph_eq /proph_def.
-    iDestruct (own_valid_2 with "H● Hp") as %[HR%proph_map_singleton_included _]%auth_valid_discrete_2.
+    iDestruct (own_valid_2 with "H● Hp") as %[HR%proph_map_singleton_included _]%auth_both_valid.
     assert (vs = v :: proph_list_resolves pvs p) as ->.
     { rewrite (Hres p vs HR). simpl. by rewrite decide_True. }
     iMod (own_update_2 with "H● Hp") as "[H● H◯]".
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index e09b59f9d14a72ce2d1070ebc19374860cf165c8..d6538bff82ef4ea3d461af873dc806a8f2dcc7c9 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -198,7 +198,7 @@ Lemma wsat_alloc `{!invPreG Σ} : (|==> ∃ _ : invG Σ, wsat ∗ ownE ⊤)%I.
 Proof.
   iIntros.
   iMod (own_alloc (● (∅ : gmap positive _))) as (γI) "HI";
-    first by rewrite -auth_auth_valid.
+    first by rewrite auth_auth_valid.
   iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
   iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
   iModIntro; iExists (WsatG _ _ _ _ γI γE γD).
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index cb65f706b59cc6c8758b196c905d1640156d4d01..cde2c0b41a6e2354cebc9610193d42884d74db07 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -37,7 +37,7 @@ Section mono_proof.
   Proof.
     iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
     iMod (own_alloc (● (O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']";
-      first by apply auth_valid_discrete_2.
+      first by apply auth_both_valid.
     iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
     iModIntro. iApply "HΦ". rewrite /mcounter; eauto 10.
@@ -54,7 +54,7 @@ Section mono_proof.
     wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
     destruct (decide (c' = c)) as [->|].
     - iDestruct (own_valid_2 with "Hγ Hγf")
-        as %[?%mnat_included _]%auth_valid_discrete_2.
+        as %[?%mnat_included _]%auth_both_valid.
       iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
       { apply auth_update, (mnat_local_update _ _ (S c)); auto. }
       wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
@@ -75,7 +75,7 @@ Section mono_proof.
     rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]".
     wp_load.
     iDestruct (own_valid_2 with "Hγ Hγf")
-      as %[?%mnat_included _]%auth_valid_discrete_2.
+      as %[?%mnat_included _]%auth_both_valid.
     iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
     { apply auth_update, (mnat_local_update _ _ c); auto. }
     iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
@@ -115,7 +115,7 @@ Section contrib_spec.
   Proof.
     iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
     iMod (own_alloc (●! O%nat ⋅ ◯! 0%nat)) as (γ) "[Hγ Hγ']";
-      first by apply auth_valid_discrete_2.
+      first by apply auth_both_valid.
     iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
     iModIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 681b7a22b9e748690f1fe27fb166a4c70b280c20..a3c6010703a90dff6299f920de677d4802cc9f06 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -76,7 +76,7 @@ Section proof.
     iIntros (Φ) "HR HΦ". rewrite -wp_fupd. wp_lam.
     wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
     iMod (own_alloc (● (Excl' 0%nat, GSet ∅) ⋅ ◯ (Excl' 0%nat, GSet ∅))) as (γ) "[Hγ Hγ']".
-    { by apply auth_valid_discrete_2. }
+    { by apply auth_both_valid. }
     iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
     { iNext. rewrite /lock_inv.
       iExists 0%nat, 0%nat. iFrame. iLeft. by iFrame. }
@@ -141,14 +141,14 @@ Section proof.
     iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)".
     wp_load.
     iDestruct (own_valid_2 with "Hauth Hγo") as
-      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
+      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid.
     iModIntro. iSplitL "Hlo Hln Hauth Haown".
     { iNext. iExists o, n. by iFrame. }
     wp_pures.
     iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)".
     iApply wp_fupd. wp_store.
     iDestruct (own_valid_2 with "Hauth Hγo") as
-      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
+      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid.
     iDestruct "Haown" as "[[Hγo' _]|Haown]".
     { iDestruct (own_valid_2 with "Hγo Hγo'") as %[[] ?]. }
     iMod (own_update_2 with "Hauth Hγo") as "[Hauth Hγo]".
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 0bbe407eeba6f29171c72072bfb371f9c432200c..4b4b4a9a20292fc6b99b4da7e912cb5f0dee4222 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -54,7 +54,7 @@ Proof.
   intros Hwp. apply (wp_adequacy Σ _).
   iIntros (? κs).
   iMod (own_alloc (● (Excl' σ) ⋅ ◯ (Excl' σ))) as (γσ) "[Hσ Hσf]";
-    first by apply auth_valid_discrete_2.
+    first by apply auth_both_valid.
   iModIntro. iExists (λ σ κs, own γσ (● (Excl' σ)))%I.
   iFrame "Hσ".
   iApply (Hwp (OwnPG _ _ _ _ γσ)). rewrite /ownP. iFrame.
@@ -70,14 +70,14 @@ Proof.
   intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
   iIntros (? κs κs').
   iMod (own_alloc (● (Excl' σ1) ⋅ ◯ (Excl' σ1))) as (γσ) "[Hσ Hσf]";
-    first by apply auth_valid_discrete_2.
+    first by apply auth_both_valid.
   iExists (λ σ κs' _, own γσ (● (Excl' σ)))%I, (λ _, True%I).
   iFrame "Hσ".
   iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]";
     first by rewrite /ownP; iFrame.
   iIntros "!> Hσ". iMod "H" as (σ2') "[Hσf %]". rewrite /ownP.
   iDestruct (own_valid_2 with "Hσ Hσf")
-    as %[Hp%Excl_included _]%auth_valid_discrete_2; simplify_eq; auto.
+    as %[Hp%Excl_included _]%auth_both_valid; simplify_eq; auto.
 Qed.
 
 
@@ -91,7 +91,7 @@ Section lifting.
   Lemma ownP_eq σ1 σ2 κs n : state_interp σ1 κs n -∗ ownP σ2 -∗ ⌜σ1 = σ2⌝.
   Proof.
     iIntros "Hσ● Hσ◯". rewrite /ownP.
-    iDestruct (own_valid_2 with "Hσ● Hσ◯") as %[Hps _]%auth_valid_discrete_2.
+    iDestruct (own_valid_2 with "Hσ● Hσ◯") as %[Hps _]%auth_both_valid.
     by pose proof (leibniz_equiv _ _ (Excl_included _ _ Hps)) as ->.
   Qed.
   Lemma ownP_state_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.