Merge branch 'robbert/auth_auth_validN' into 'master'

Fix direction of `auth_auth_validN`

See merge request iris/iris!515

CHANGELOG.md

@@ -20,6 +20,8 @@ With this release, we dropped support for Coq 8.9.
   (`iso_cmra_mixin_restrict`) and through an isomorphism (`iso_cmra_mixin`).
 * Add a `frac_agree` library which encapsulates `frac * agree A` for some OFE
   `A`, and provides some useful lemmas.
+* Fix direction of `auth_auth_validN` to make it consistent with similar lemmas,
+  e.g., `auth_auth_valid`. The direction is now `✓{n} (● a) ↔ ✓{n} a`.
 
 **Changes in `proofmode`:**
 

theories/algebra/auth.v

@@ -162,7 +162,7 @@ Proof.
   - by intros [?[->%(inj to_agree) []]].
   - naive_solver eauto using ucmra_unit_leastN.
 Qed.
-Lemma auth_auth_validN n a : ✓{n} a ↔ ✓{n} (● a).
+Lemma auth_auth_validN n a : ✓{n} (● a) ↔ ✓{n} a.
 Proof.
   rewrite auth_auth_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
 Qed.