diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 6e201a88958c3de7515bccc66b8a17e5e4aa261a..859cdad2ec948580001708d72aa0809dab2f6eaf 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -96,6 +96,11 @@ Class Cofe (A : ofeT) := {
 }.
 Arguments compl : simpl never.
 
+Lemma compl_chain_map `{Cofe A, Cofe B} (f : A → B) c
+      `(∀ n : nat, Proper (dist n ==> dist n) f) :
+  compl (chain_map f c) ≡ f (compl c).
+Proof. apply equiv_dist=>n. by rewrite !conv_compl. Qed.
+
 (** General properties *)
 Section cofe.
   Context {A : ofeT}.