From f2450784c5b3a8bb172457e97fb8ec971817254c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 24 Aug 2016 11:27:22 +0200
Subject: [PATCH] Put now_True_rvs near derived properties (since it _is_
 derived).

---
 algebra/upred.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/algebra/upred.v b/algebra/upred.v
index df3809e30..8f04cdf1e 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.
-- 
GitLab