Make validy lemmas for `excl_auth` more consistent with `auth`.

- Rename `excl_auth_frag_validN_op_1_l` into `excl_auth_frag_op_validN` and
  `excl_auth_frag_valid_op_1_l` into `excl_auth_frag_op_valid` (similar to
  `auth_auth_op_valid`, and make them bi-implications.
- Add `excl_auth_auth_op_validN` and `excl_auth_auth_op_valid`

iris/algebra/lib/excl_auth.v

@@ -59,9 +59,14 @@ Section excl_auth.
   Lemma excl_auth_agree_L `{!LeibnizEquiv A} a b : ✓ (●E a ⋅ ◯E b) → a = b.
   Proof. intros. by apply leibniz_equiv, excl_auth_agree. Qed.
 
-  Lemma excl_auth_frag_validN_op_1_l n a b : ✓{n} (◯E a ⋅ ◯E b) → False.
+  Lemma excl_auth_auth_op_validN n a b : ✓{n} (●E a ⋅ ●E b) ↔ False.
+  Proof. apply auth_auth_op_validN. Qed.
+  Lemma excl_auth_auth_op_valid a b : ✓ (●E a ⋅ ●E b) ↔ False.
+  Proof. apply auth_auth_op_valid. Qed.
+
+  Lemma excl_auth_frag_op_validN n a b : ✓{n} (◯E a ⋅ ◯E b) ↔ False.
   Proof. by rewrite -auth_frag_op auth_frag_validN. Qed.
-  Lemma excl_auth_frag_valid_op_1_l a b : ✓ (◯E a ⋅ ◯E b) → False.
+  Lemma excl_auth_frag_op_valid a b : ✓ (◯E a ⋅ ◯E b) ↔ False.
   Proof. by rewrite -auth_frag_op auth_frag_valid. Qed.
 
   Lemma excl_auth_update a b a' : ●E a ⋅ ◯E b ~~> ●E a' ⋅ ◯E a'.

iris/program_logic/ownp.v

@@ -100,7 +100,7 @@ Section lifting.
   Qed.
   Lemma ownP_state_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
   Proof.
-    rewrite /ownP -own_op own_valid. by iIntros (?%excl_auth_frag_valid_op_1_l).
+    rewrite /ownP -own_op own_valid. by iIntros (?%excl_auth_frag_op_valid).
   Qed.
   Global Instance ownP_timeless σ : Timeless (@ownP Λ Σ _ σ).
   Proof. rewrite /ownP; apply _. Qed.