Rename auth_both_frac_op to auth_both_op

Removes auth_both_op and renames auth_both_frac_op into auth_both_op.

CHANGELOG.md

@@ -150,6 +150,7 @@ Coq development, but not every API-breaking change is listed.  Changes marked
     - `|={E1,E2}|>=>^n Q` for `|={E1,E2}▷=>^n Q`
     The full list can be found in [theories/bi/ascii.v](theories/bi/ascii.v),
     where the ASCII notations are defined in terms of the unicode notations.
+* Removed `auth_both_op` and renamed `auth_both_frac_op` into `auth_both_op`.
 
 The following `sed` script should perform most of the renaming (FIXME: incomplete)
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
@@ -167,6 +168,8 @@ s/\blist_lookup_singletonM(|_lt|_gt|_ne)\b/list_lookup_singleton\1/g
 s/\blist_singletonM_(validN|length)\b/list_singleton_\1/g
 s/\blist_alter_singletonM\b/list_alter_singleton/g
 s/\blist_singletonM_included\b/list_singleton_included/g
+# auth_both_frac_op rename
+s/\bauth_both_frac_op\b/auth_both_op/g
 ' $(find theories -name "*.v")
 ```
 

theories/algebra/auth.v

@@ -306,10 +306,8 @@ 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.
 
-Lemma auth_both_frac_op q a b : Auth (Some (q,to_agree a)) b ≡ ●{q} a ⋅ ◯ b.
+Lemma auth_both_op q a b : Auth (Some (q,to_agree a)) b ≡ ●{q} a ⋅ ◯ b.
 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 + q} a ≡ ●{p} a ⋅ ●{q} a.
 Proof.
@@ -348,7 +346,7 @@ Proof. by rewrite auth_validI. Qed.
 Lemma auth_both_validI {M} q (a b: A) :
   ✓ (●{q} a ⋅ ◯ b) ⊣⊢@{uPredI M} ✓ q ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
 Proof.
-  rewrite -auth_both_frac_op auth_validI /=. apply bi.and_proper; [done|].
+  rewrite -auth_both_op auth_validI /=. apply bi.and_proper; [done|].
   setoid_rewrite agree_equivI. iSplit.
   - iDestruct 1 as (a') "[#Eq [H V]]". iDestruct "H" as (b') "H".
     iRewrite -"Eq" in "H". iRewrite -"Eq" in "V". auto.