From 728bf3ba39f8c16d39bc7378b1d7fd22b04f4374 Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Wed, 22 Apr 2020 12:29:47 +0200
Subject: [PATCH] Apply suggestion to theories/algebra/agree.v

---
 theories/algebra/agree.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 1d4c4d38d..84fb02731 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -207,7 +207,7 @@ Proof.
   by move=> /agree_op_invN->; rewrite agree_idemp.
 Qed.
 
-Lemma to_agree_includedN n a b : to_agree a ≼{n}to_agree b ↔ a ≡{n}≡ b.
+Lemma to_agree_includedN n a b : to_agree a ≼{n} to_agree b ↔ a ≡{n}≡ b.
 Proof.
   split; last by intros ->.
   intros (x & Heq). destruct Heq as [_ Hincl].
-- 
GitLab