add later_ne; make later_proper match the other _proper lemmas

theories/base_logic/derived.v

@@ -672,9 +672,9 @@ Proof.
 Qed.
 
 (* Later derived *)
-Lemma later_proper P Q : (P ⊣⊢ Q) → ▷ P ⊣⊢ ▷ Q.
+Lemma later_proper' P Q : (P ⊣⊢ Q) → ▷ P ⊣⊢ ▷ Q.
 Proof. by intros ->. Qed.
-Hint Resolve later_mono later_proper.
+Hint Resolve later_mono later_proper'.
 Global Instance later_mono' : Proper ((⊢) ==> (⊢)) (@uPred_later M).
 Proof. intros P Q; apply later_mono. Qed.
 Global Instance later_flip_mono' :

theories/base_logic/primitive.v

@@ -307,7 +307,8 @@ Proof.
   unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try omega.
   apply HPQ; eauto using cmra_validN_S.
 Qed.
-Global Instance later_proper' :
+Definition later_ne : NonExpansive (@uPred_later M) := _.
+Global Instance later_proper :
   Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_later M) := ne_proper _.
 Global Instance plainly_ne : NonExpansive (@uPred_plainly M).
 Proof.