diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index fc6f1806f35683bcd7c33a1522f24a70ca89b1f2..4498827656cfc59e8617ed895693fb7d97457fdd 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -100,11 +100,71 @@ Section auth.
   Global Instance auth_frag_inj : Inj (â‰¡) (â‰¡) (@auth_frag A).
   Proof. rewrite /auth_frag. apply _. Qed.
 
+  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).
+  Proof. rewrite /auth_auth. apply _. Qed.
+  Global Instance auth_frag_discrete a : Discrete a â†’ Discrete (â—¯ a).
+  Proof. rewrite /auth_frag. apply _. Qed.
+  Global Instance auth_cmra_discrete : CmraDiscrete A â†’ CmraDiscrete (authR A).
+  Proof. apply _. Qed.
+
+  (** Operation *)
+  Lemma auth_auth_frac_op p q a : â—{p + q} a â‰¡ â—{p} a â‹… â—{q} 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).
+  Proof. rewrite /auth_auth. apply _. Qed.
+
+  Lemma auth_frag_op a b : â—¯ (a â‹… b) = â—¯ a â‹… â—¯ b.
+  Proof. apply view_frag_op. Qed.
+  Lemma auth_frag_mono a b : a â‰¼ b â†’ â—¯ a â‰¼ â—¯ b.
+  Proof. apply view_frag_mono. Qed.
+  Lemma auth_frag_core a : core (â—¯ a) = â—¯ (core a).
+  Proof. apply view_frag_core. Qed.
+  Global Instance auth_frag_core_id a : CoreId a â†’ CoreId (â—¯ a).
+  Proof. rewrite /auth_frag. apply _. Qed.
+  Global Instance auth_frag_is_op a b1 b2 :
+    IsOp a b1 b2 â†’ IsOp' (â—¯ a) (â—¯ b1) (â—¯ b2).
+  Proof. rewrite /auth_frag. apply _. Qed.
+  Global Instance auth_frag_sep_homomorphism :
+    MonoidHomomorphism op op (â‰¡) (@auth_frag A).
+  Proof. rewrite /auth_frag. apply _. Qed.
+
+  Lemma big_opL_auth_frag {B} (g : nat â†’ B â†’ A) (l : list B) :
+    (â—¯ [^op list] kâ†¦x âˆˆ l, g k x) â‰¡ [^op list] kâ†¦x âˆˆ l, â—¯ (g k x).
+  Proof. apply (big_opL_commute _). Qed.
+  Lemma big_opM_auth_frag `{Countable K} {B} (g : K â†’ B â†’ A) (m : gmap K B) :
+    (â—¯ [^op map] kâ†¦x âˆˆ m, g k x) â‰¡ [^op map] kâ†¦x âˆˆ m, â—¯ (g k x).
+  Proof. apply (big_opM_commute _). Qed.
+  Lemma big_opS_auth_frag `{Countable B} (g : B â†’ A) (X : gset B) :
+    (â—¯ [^op set] x âˆˆ X, g x) â‰¡ [^op set] x âˆˆ X, â—¯ (g x).
+  Proof. apply (big_opS_commute _). Qed.
+  Lemma big_opMS_auth_frag `{Countable B} (g : B â†’ A) (X : gmultiset B) :
+    (â—¯ [^op mset] x âˆˆ X, g x) â‰¡ [^op mset] x âˆˆ X, â—¯ (g x).
+  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.
+  Proof. apply view_auth_frac_op_invN. Qed.
+  Lemma auth_auth_frac_op_inv p a q b : âœ“ (â—{p} a â‹… â—{q} 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.
+  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.
   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.
+  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.
+
   (** The following lemmas are also stated as implications, which can be used
   to force [apply] to use the lemma in the right direction. *)
   Lemma auth_frag_validN n b : âœ“{n} (â—¯ b) â†” âœ“{n} b.
@@ -137,6 +197,15 @@ Section auth.
     by setoid_rewrite auth_view_rel_unit.
   Qed.
 
+  Lemma auth_auth_frac_op_valid q1 q2 a1 a2 :
+    âœ“ (â—{q1} a1 â‹… â—{q2} a2) â†” âœ“ (q1 + q2)%Qp âˆ§ a1 â‰¡ a2 âˆ§ âœ“ a1.
+  Proof.
+    rewrite view_auth_frac_op_valid !cmra_valid_validN.
+    by setoid_rewrite auth_view_rel_unit.
+  Qed.
+  Lemma auth_auth_op_valid a1 a2 : âœ“ (â— a1 â‹… â— a2) â†” False.
+  Proof. apply view_auth_op_valid. Qed.
+
   (** The following lemmas are also stated as implications, which can be used
   to force [apply] to use the lemma in the right direction. *)
   Lemma auth_frag_valid b : âœ“ (â—¯ b) â†” âœ“ b.
@@ -191,57 +260,6 @@ Section auth.
     âœ“ (â— a â‹… â—¯ b) â†” b â‰¼ a âˆ§ âœ“ a.
   Proof. rewrite auth_both_frac_valid_discrete frac_valid'. naive_solver. Qed.
 
-  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).
-  Proof. rewrite /auth_auth. apply _. Qed.
-  Global Instance auth_frag_discrete a : Discrete a â†’ Discrete (â—¯ a).
-  Proof. rewrite /auth_frag. apply _. Qed.
-  Global Instance auth_cmra_discrete : CmraDiscrete A â†’ CmraDiscrete (authR A).
-  Proof. apply _. Qed.
-
-  Lemma auth_auth_frac_op p q a : â—{p + q} a â‰¡ â—{p} a â‹… â—{q} a.
-  Proof. apply view_auth_frac_op. Qed.
-  Lemma auth_auth_frac_op_invN n p a q b : âœ“{n} (â—{p} a â‹… â—{q} 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.
-  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.
-  Proof. by apply view_auth_frac_op_inv_L. Qed.
-  Global Instance auth_auth_frac_is_op q q1 q2 a :
-    IsOp q q1 q2 â†’ IsOp' (â—{q} a) (â—{q1} a) (â—{q2} a).
-  Proof. rewrite /auth_auth. apply _. Qed.
-
-  Lemma auth_frag_op a b : â—¯ (a â‹… b) = â—¯ a â‹… â—¯ b.
-  Proof. apply view_frag_op. Qed.
-  Lemma auth_frag_mono a b : a â‰¼ b â†’ â—¯ a â‰¼ â—¯ b.
-  Proof. apply view_frag_mono. Qed.
-  Lemma auth_frag_core a : core (â—¯ a) = â—¯ (core a).
-  Proof. apply view_frag_core. Qed.
-  Global Instance auth_frag_core_id a : CoreId a â†’ CoreId (â—¯ a).
-  Proof. rewrite /auth_frag. apply _. Qed.
-  Global Instance auth_frag_is_op a b1 b2 :
-    IsOp a b1 b2 â†’ IsOp' (â—¯ a) (â—¯ b1) (â—¯ b2).
-  Proof. rewrite /auth_frag. apply _. Qed.
-  Global Instance auth_frag_sep_homomorphism :
-    MonoidHomomorphism op op (â‰¡) (@auth_frag A).
-  Proof. rewrite /auth_frag. apply _. Qed.
-
-  Lemma big_opL_auth_frag {B} (g : nat â†’ B â†’ A) (l : list B) :
-    (â—¯ [^op list] kâ†¦x âˆˆ l, g k x) â‰¡ [^op list] kâ†¦x âˆˆ l, â—¯ (g k x).
-  Proof. apply (big_opL_commute _). Qed.
-  Lemma big_opM_auth_frag `{Countable K} {B} (g : K â†’ B â†’ A) (m : gmap K B) :
-    (â—¯ [^op map] kâ†¦x âˆˆ m, g k x) â‰¡ [^op map] kâ†¦x âˆˆ m, â—¯ (g k x).
-  Proof. apply (big_opM_commute _). Qed.
-  Lemma big_opS_auth_frag `{Countable B} (g : B â†’ A) (X : gset B) :
-    (â—¯ [^op set] x âˆˆ X, g x) â‰¡ [^op set] x âˆˆ X, â—¯ (g x).
-  Proof. apply (big_opS_commute _). Qed.
-  Lemma big_opMS_auth_frag `{Countable B} (g : B â†’ A) (X : gmultiset B) :
-    (â—¯ [^op mset] x âˆˆ X, g x) â‰¡ [^op mset] x âˆˆ X, â—¯ (g x).
-  Proof. apply (big_opMS_commute _). Qed.
-
   (** Inclusion *)
   Lemma auth_auth_frac_includedN n p1 p2 a1 a2 b :
     â—{p1} a1 â‰¼{n} â—{p2} a2 â‹… â—¯ b â†” (p1 â‰¤ p2)%Qc âˆ§ a1 â‰¡{n}â‰¡ a2.
diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v
index 879c029e9c5dc54da4ff86b87a19b5c9bab1459a..7cc89e9901605b667a5292486a854417d83cdea1 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/theories/algebra/lib/gmap_view.v
@@ -108,6 +108,9 @@ Section rel.
     - intros k'. rewrite !lookup_insert_None. naive_solver.
   Qed.
 
+  Local Lemma gmap_view_rel_unit n m : gmap_view_rel n m Îµ.
+  Proof. apply: map_Forall_empty. Qed.
+
   Local Lemma gmap_view_rel_discrete :
     OfeDiscrete V â†’ ViewRelDiscrete gmap_view_rel.
   Proof.
@@ -174,18 +177,13 @@ Section lemmas.
   Qed.
 
   (** Composition and validity *)
-  Lemma gmap_view_auth_frac_valid m q : âœ“ gmap_view_auth q m â†” âœ“ q.
-  Proof.
-    rewrite view_auth_frac_valid. split; first by naive_solver.
-    intros. split; first done.
-    intros n l ? Hl. rewrite lookup_empty in Hl. done.
-  Qed.
-  Lemma gmap_view_auth_valid m : âœ“ gmap_view_auth 1 m.
-  Proof. rewrite gmap_view_auth_frac_valid. done. Qed.
-
   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.
+  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.
+
   Lemma gmap_view_auth_frac_op_invN n p m1 q m2 :
     âœ“{n} (gmap_view_auth p m1 â‹… gmap_view_auth q m2) â†’ m1 â‰¡{n}â‰¡ m2.
   Proof. apply view_auth_frac_op_invN. Qed.
@@ -195,9 +193,22 @@ Section lemmas.
   Lemma gmap_view_auth_frac_op_inv_L `{!LeibnizEquiv V} q m1 p m2 :
     âœ“ (gmap_view_auth p m1 â‹… gmap_view_auth q m2) â†’ m1 = m2.
   Proof. apply view_auth_frac_op_inv_L, _. 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.
+
+  Lemma gmap_view_auth_frac_valid m q : âœ“ gmap_view_auth q m â†” âœ“ q.
+  Proof.
+    rewrite view_auth_frac_valid. intuition eauto using gmap_view_rel_unit.
+  Qed.
+  Lemma gmap_view_auth_valid m : âœ“ gmap_view_auth 1 m.
+  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.
+  Proof.
+    rewrite view_auth_frac_op_valid. intuition eauto using gmap_view_rel_unit.
+  Qed.
+  Lemma gmap_view_auth_op_valid m1 m2 :
+    âœ“ (gmap_view_auth 1 m1 â‹… gmap_view_auth 1 m2) â†” False.
+  Proof. apply view_auth_op_valid. Qed.
 
   Lemma gmap_view_frag_validN n k dq v : âœ“{n} gmap_view_frag k dq v â†” âœ“ dq.
   Proof.
@@ -256,8 +267,8 @@ Section lemmas.
     rewrite view_both_frac_valid. setoid_rewrite gmap_view_rel_lookup.
     split=>[[Hq Hm]|[Hq Hm]].
     - split; first done. split.
-      +  apply (Hm 0%nat).
-      +  apply equiv_dist=>n. apply Hm.
+      + apply (Hm 0%nat).
+      + apply equiv_dist=>n. apply Hm.
     - split; first done. split.
       + apply Hm.
       + revert n. apply equiv_dist. apply Hm.
diff --git a/theories/algebra/view.v b/theories/algebra/view.v
index 89954f77ee2ab964bc7619582c150eb13daacf68..ab718ce3b100123b2831a1e083724f0a3928b013 100644
--- a/theories/algebra/view.v
+++ b/theories/algebra/view.v
@@ -204,47 +204,6 @@ Section cmra.
       | None => âˆƒ a, rel n a (view_frag_proj x)
       end := eq_refl _.
 
-  Lemma view_auth_frac_validN n q a : âœ“{n} (â—V{q} a) â†” âœ“{n} q âˆ§ 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.
-  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) â†” âœ“{n} q âˆ§ 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.
-
-  Lemma view_auth_frac_valid q a : âœ“ (â—V{q} a) â†” âœ“ q âˆ§ âˆ€ 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.
-  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.
-  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.
-
   Lemma view_cmra_mixin : CmraMixin (view rel).
   Proof.
     apply (iso_cmra_mixin_restrict
@@ -304,25 +263,12 @@ Section cmra.
   Qed.
   Canonical Structure viewUR := UcmraT (view rel) view_ucmra_mixin.
 
+  (** Operation *)
   Lemma view_auth_frac_op p1 p2 a : â—V{p1 + p2} a â‰¡ â—V{p1} a â‹… â—V{p2} a.
   Proof.
     intros; split; simpl; last by rewrite left_id.
     by rewrite -Some_op -pair_op agree_idemp.
   Qed.
-  Lemma view_auth_frac_op_invN n p1 a1 p2 a2 :
-    âœ“{n} (â—V{p1} a1 â‹… â—V{p2} a2) â†’ a1 â‰¡{n}â‰¡ a2.
-  Proof.
-    rewrite /op /view_op /= 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.
-  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.
-  Proof. by intros ?%view_auth_frac_op_inv%leibniz_equiv. 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).
   Proof. rewrite /IsOp' /IsOp => ->. by rewrite -view_auth_frac_op. Qed.
@@ -355,6 +301,87 @@ Section cmra.
     (â—¯V [^op mset] x âˆˆ X, g x) â‰¡ [^op mset] x âˆˆ X, â—¯V (g x).
   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.
+  Proof.
+    rewrite /op /view_op /= 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.
+  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.
+  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 Îµ.
+  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.
+
+  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 Îµ.
+  Proof.
+    split.
+    - intros Hval. assert (a1 â‰¡{n}â‰¡ a2) as Ha by eauto using view_auth_frac_op_invN.
+      revert Hval. rewrite Ha -view_auth_frac_op view_auth_frac_validN. naive_solver.
+    - intros (?&->&?). by rewrite -view_auth_frac_op view_auth_frac_validN.
+  Qed.
+  Lemma view_auth_op_validN n a1 a2 : âœ“{n} (â—V a1 â‹… â—V a2) â†” False.
+  Proof. rewrite view_auth_frac_op_validN. naive_solver. Qed.
+
+  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) â†” âœ“{n} q âˆ§ 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.
+
+  Lemma view_auth_frac_valid q a : âœ“ (â—V{q} a) â†” âœ“ q âˆ§ âˆ€ 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.
+
+  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 Îµ.
+  Proof.
+    rewrite !cmra_valid_validN equiv_dist. setoid_rewrite view_auth_frac_op_validN.
+    setoid_rewrite <-cmra_discrete_valid_iff. naive_solver.
+  Qed.
+  Lemma view_auth_op_valid a1 a2 : âœ“ (â—V a1 â‹… â—V a2) â†” False.
+  Proof. rewrite view_auth_frac_op_valid. naive_solver. Qed.
+
+  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.
+  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.
+
   (** Inclusion *)
   Lemma view_auth_frac_includedN n p1 p2 a1 a2 b :
     â—V{p1} a1 â‰¼{n} â—V{p2} a2 â‹… â—¯V b â†” (p1 â‰¤ p2)%Qc âˆ§ a1 â‰¡{n}â‰¡ a2.