diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 1d4c4d38de24f7675fcd4ae0d2a87bc16c92bfb8..84fb027315fd1140caae8e1282a710243d7d2e43 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].