From 28761b214648c32ffce9154ff5d224f1b3c57f29 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Thu, 5 Jan 2017 16:20:01 +0100
Subject: [PATCH] Add lemma compl_chain_map.

---
 theories/algebra/ofe.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 6e201a889..859cdad2e 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}.
-- 
GitLab