diff --git a/algebra/upred.v b/algebra/upred.v
index df3809e304be2f689c12b9d8de9c04dd1be6c06e..8f04cdf1ea80198fa0831e02a2bb6dd830ca806c 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1181,11 +1181,6 @@ Proof.
   exists (y â‹… x3); split; first by rewrite -assoc.
   exists y; eauto using cmra_includedN_l.
 Qed.
-Lemma now_True_rvs P : ◇ (|=r=> P) ⊢ (|=r=> ◇ P).
-Proof.
-  rewrite /uPred_now_True. apply or_elim; auto using rvs_mono.
-  by rewrite -rvs_intro -or_intro_l.
-Qed.
 
 (** * Derived rules *)
 Global Instance rvs_mono' : Proper ((⊢) ==> (⊢)) (@uPred_rvs M).
@@ -1205,6 +1200,11 @@ Proof.
   intros; rewrite (rvs_ownM_updateP _ (y =)); last by apply cmra_update_updateP.
   by apply rvs_mono, exist_elim=> y'; apply pure_elim_l=> ->.
 Qed.
+Lemma now_True_rvs P : ◇ (|=r=> P) ⊢ (|=r=> ◇ P).
+Proof.
+  rewrite /uPred_now_True. apply or_elim; auto using rvs_mono.
+  by rewrite -rvs_intro -or_intro_l.
+Qed.
 
 (* Products *)
 Lemma prod_equivI {A B : cofeT} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.