diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 1fc18c69f3d2ea3b51193b0a85d4d04ede9dfb71..1b61b0be8ca33a22d72b57d2e18b323f2038f6f2 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -290,7 +290,8 @@ Section limit_preserving.
   Proof. intros PH c Hc. by rewrite (conv_compl 0). Qed.
 
   Lemma limit_preserving_and (P1 P2 : A → Prop) :
-    LimitPreserving P1 → LimitPreserving P2 →
+    LimitPreserving P1 →
+    LimitPreserving P2 →
     LimitPreserving (λ x, P1 x ∧ P2 x).
   Proof.
     intros Hlim1 Hlim2 c Hc.
@@ -300,7 +301,8 @@ Section limit_preserving.
   Qed.
 
   Lemma limit_preserving_impl (P1 P2 : A → Prop) :
-    Proper (dist 0 ==> impl) P1 → LimitPreserving P2 →
+    Proper (dist 0 ==> impl) P1 →
+    LimitPreserving P2 →
     LimitPreserving (λ x, P1 x → P2 x).
   Proof.
     intros Hlim1 Hlim2 c Hc HP1. apply Hlim2=> n; apply Hc.
@@ -310,7 +312,8 @@ Section limit_preserving.
   (** This is strictly weaker than the [_impl] variant, but sometimes automation
       is better at proving [Proper] for [iff] than for [impl]. *)
   Lemma limit_preserving_iff (P1 P2 : A → Prop) :
-    Proper (dist 0 ==> iff) P1 → LimitPreserving P2 →
+    Proper (dist 0 ==> iff) P1 →
+    LimitPreserving P2 →
     LimitPreserving (λ x, P1 x → P2 x).
   Proof.
     intros HP1. apply limit_preserving_impl. intros ???.