diff --git a/modures/cofe.v b/modures/cofe.v
index 5f1e2a4c3ea027bb5db03080cf60854f85237897..1b8913b96f73a28e2e3877142268fa9e8aae03b7 100644
--- a/modures/cofe.v
+++ b/modures/cofe.v
@@ -334,6 +334,8 @@ Section later.
   Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
   Global Instance Later_contractive : Contractive (@Later A).
   Proof. by intros n ??. Qed.
+  Global Instance Later_inj n : Injective (dist n) (dist (S n)) (@Later A).
+  Proof. by intros x y. Qed.
 End later.
 
 Arguments laterC : clear implicits.