diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index b8b184c06eb92f6d04ee306319829a985d28c910..b535887c0cedd905bba17d0bb0692169e82a5664 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -170,11 +170,20 @@ Proof. by rewrite /FromAlways. Qed.
 Global Instance into_laterN_later n P Q :
   IntoLaterN n P Q → IntoLaterN' (S n) (▷ P) Q.
 Proof. by rewrite /IntoLaterN' /IntoLaterN =>->. Qed.
+Global Instance into_laterN_later_further n P Q :
+  IntoLaterN' n P Q → IntoLaterN' n (▷ P) (▷ Q).
+Proof. rewrite /IntoLaterN' /IntoLaterN =>->. by rewrite -laterN_later. Qed.
+
 Global Instance into_laterN_laterN n P : IntoLaterN' n (â–·^n P) P.
 Proof. done. Qed.
 Global Instance into_laterN_laterN_plus n m P Q :
   IntoLaterN m P Q → IntoLaterN' (n + m) (▷^n P) Q.
 Proof. rewrite /IntoLaterN' /IntoLaterN=>->. by rewrite laterN_plus. Qed.
+Global Instance into_laterN_laterN_further n m P Q :
+  IntoLaterN' m P Q → IntoLaterN' m (▷^n P) (▷^n Q).
+Proof.
+  rewrite /IntoLaterN' /IntoLaterN=>->. by rewrite -!laterN_plus Nat.add_comm.
+Qed.
 
 Global Instance into_laterN_and_l n P1 P2 Q1 Q2 :
   IntoLaterN' n P1 Q1 → IntoLaterN n P2 Q2 →