From c5008933e4f17c122a0b23e6e6cfe8d198423214 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 17 Jun 2020 14:09:03 +0200
Subject: fixup spacing

---
 mathcomp/ssreflect/fintype.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 986d9fd..3705530 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -814,7 +814,7 @@ by split=> // z; rewrite !inE => /pred2P[]->.
 Qed.
 
 Lemma card_gt2P A :
-  reflect (exists x y z, [/\ x \in A, y \in A & z \in A] /\ [/\ x!=y, y!=z & z!=x])
+  reflect (exists x y z, [/\ x \in A, y \in A & z \in A] /\ [/\ x != y, y != z & z != x])
           (2 < #|A|).
 Proof.
 apply: (iffP card_geqP) => [[s] []|[x] [y] [z] [[xD yD zD] [xDy xDz yDz]]].
-- 
cgit v1.2.3