diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index eeefadec882b0bee0a0508a3747e5cc386d9825e..7a722900b4afbd9f56191fc4e167994b0f92ff1a 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -189,6 +189,9 @@ Arguments dist_later _ !_ _ _ /.
 Global Instance dist_later_equivalence A n : Equivalence (@dist_later A n).
 Proof. destruct n as [|n]. by split. apply dist_equivalence. Qed.
 
+Lemma dist_dist_later {A : ofeT} n (x y : A) : dist n x y → dist_later n x y.
+Proof. intros Heq. destruct n; first done. exact: dist_S. Qed.
+
 Notation Contractive f := (∀ n, Proper (dist_later n ==> dist n) f).
 
 Instance const_contractive {A B : ofeT} (x : A) : Contractive (@const A B x).