CmraSwappable also implies ▷ commutes with -∗ and |==>

Commuting with |==> would have been interesting a bunch of times. But I still
don't see a way to commute with fancy updates, even mask-preserving ones.

theories/base_logic/upred.v

@@ -671,6 +671,46 @@ Proof.
     by rewrite -Hnx'x''.
 Qed.
 
+Lemma later_wand `{!CmraSwappable M} P Q : (▷ P -∗ ▷ Q) ⊢ ▷ (P -∗ Q).
+Proof.
+  unseal; split => /= -[//|n] x ? HPQ n' x' ?? HP.
+  specialize (HPQ (S n')); cbn in HPQ.
+  case: (cmra_extend_included n' (Some x) x') => [||x'' []];
+    rewrite /= ?(comm _ _ x) ?Some_validN //.
+  - by eapply cmra_validN_le; eauto.
+  - move => ? Hnx'x''.
+    rewrite Hnx'x''. apply HPQ; eauto.
+    by rewrite -Hnx'x''.
+Qed.
+
+Lemma later_bupd `{!CmraSwappable M} P : (▷ |==> P) ⊢ |==> ▷ P.
+Proof.
+  unseal; split => /= -[|n] x ? HP k yf Hkl.
+  - have ->: k = 0 by lia. by eauto.
+  - case: (decide (k ≤ n)) Hkl => [Hle _ Hv|Hn Hkl].
+    + case (HP k yf Hle Hv) => [x' [Hv' HP']]. exists x'; split_and! => //.
+      case: k Hle {Hv Hv'} HP' => [//|]. eauto using uPred_mono.
+    + have ->: k = S n by lia. move => {Hn Hkl} Hv.
+      case (HP n yf) => [||x' [Hv' HP']]; eauto using cmra_validN_le.
+      case: (cmra_extend_included n (Some yf) x') => [||x'' []];
+      rewrite /= ?(comm _ _ x) ?Some_validN; eauto using cmra_validN_op_r.
+      move => Hv'' Hnx'x''.
+      exists x''; split; first done.
+      by rewrite -Hnx'x''.
+Qed.
+
+Lemma bupd_later `{!CmraSwappable M} P : (|==> ▷ P) ⊢ ▷ |==> P.
+Proof.
+  unseal; split => /= -[//|n] x ? HP k yf Hkl Hv.
+  case: (cmra_extend_included k (Some x) yf) => [||yf' []];
+    rewrite /= ?(comm _ _ x) ?Some_validN //.
+  - by eapply cmra_validN_le; eauto.
+  - move => ? HyfEq.
+    case (HP (S k) yf') => [||x' [Hv' HP']]; eauto.
+    exists x'; rewrite HyfEq; split_and!;
+    eauto using cmra_validN_le.
+Qed.
+
 (** Later *)
 Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
 Proof.