diff --git a/algebra/ofe.v b/algebra/ofe.v
index 0419aa3d72ad05e9bceab1cd5e9e115c565ba43d..a24756ca26e81fc5d684b5dbf242f7cfbc39ad85 100644
--- a/algebra/ofe.v
+++ b/algebra/ofe.v
@@ -875,6 +875,7 @@ Section later.
     Proper (dist n ==> dist_later n) later_car.
   Proof. move=> [x] [y] /= Hxy. done. Qed.
 
+  (* f is contractive iff it can factor into `Next` and a non-expansive function. *)
   Lemma contractive_alt {B : ofeT} (f : A → B) :
     Contractive f ↔ ∃ g : later A → B,
       (∀ n, Proper (dist n ==> dist n) g) ∧ (∀ x, f x ≡ g (Next x)).