diff --git a/algebra/ofe.v b/algebra/ofe.v
index d979299f0e506dc993c8ca3e66201cdc6cdbb814..06ca77883ceb17e45c582660d33849531c95afd5 100644
--- a/algebra/ofe.v
+++ b/algebra/ofe.v
@@ -874,6 +874,10 @@ Section later.
   Lemma contractive_alt {B : ofeT} (f : A → B) :
     Contractive f ↔ (∀ n x y, Next x ≡{n}≡ Next y → f x ≡{n}≡ f y).
   Proof. done. Qed.
+
+  Lemma later_car_anti_contractive :
+    ∀ n, Proper (dist n ==> dist_later n) later_car.
+  Proof. move=> n [x] [y] /= Hxy. done. Qed.
 End later.
 
 Arguments laterC : clear implicits.