Replace eqVneq with eqPsym

Also changed eqsVneq.

3 files changed, 12 insertions, 13 deletions

diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 75a04ef..e4e0003 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -196,14 +196,14 @@ Proof. exact/eqP/eqP. Qed.
 
 Hint Resolve eq_refl eq_sym : core.
 
-Variant eq_xor_neq_sym (T : eqType) (x y : T) : bool -> bool -> Set :=
-  | EqNotNeqSym of x = y : eq_xor_neq_sym x y true true
-  | NeqNotEqSym of x != y : eq_xor_neq_sym x y false false.
+Variant eq_xor_neq (T : eqType) (x y : T) : bool -> bool -> Set :=
+  | EqNotNeq of x = y : eq_xor_neq x y true true
+  | NeqNotEq of x != y : eq_xor_neq x y false false.
 
-Lemma eqPsym (T : eqType) (x y : T) : eq_xor_neq_sym x y (y == x) (x == y).
+Lemma eqVneq (T : eqType) (x y : T) : eq_xor_neq x y (y == x) (x == y).
 Proof. by rewrite eq_sym; case: eqP=> [|/eqP]; constructor. Qed.
 
-Arguments eqPsym {T x y}.
+Arguments eqVneq {T} x y, {T x y}.
 
 Section Contrapositives.
 
@@ -379,9 +379,6 @@ Proof. by move->; rewrite eqxx. Qed.
 Lemma predU1r : b -> (x == y) || b.
 Proof. by move->; rewrite orbT. Qed.
 
-Lemma eqVneq : {x = y} + {x != y}.
-Proof. by case: eqP; [left | right]. Qed.
-
 End EqPred.
 
 Arguments predU1P {T x y b}.
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 204843a..c01fb39 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -232,14 +232,16 @@ Definition setTfor (phT : phant T) := [set x : T | true].
 Lemma in_setT x : x \in setTfor (Phant T).
 Proof. by rewrite in_set. Qed.
 
-Lemma eqsVneq A B : {A = B} + {A != B}.
-Proof. exact: eqVneq. Qed.
+Lemma eqsVneq A B : eq_xor_neq A B (B == A) (A == B).
+Proof. by apply: eqVneq. Qed.
 
 Lemma eq_finset (pA pB : pred T) : pA =1 pB -> finset pA = finset pB.
 Proof. by move=> eq_p; apply/setP => x; rewrite !(in_set, inE) eq_p. Qed.
 
 End BasicSetTheory.
 
+Arguments eqsVneq {T} A B, {T A B}.
+
 Definition inE := (in_set, inE).
 
 Arguments set0 {T}.
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 2ed0ee1..9581a95 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -1191,7 +1191,7 @@ Proof. by rewrite -has_pred1 has_count -eqn0Ngt; apply: eqP. Qed.
 Lemma count_uniq_mem s x : uniq s -> count_mem x s = (x \in s).
 Proof.
 elim: s => //= y s IHs /andP[/negbTE s'y /IHs-> {IHs}].
-by rewrite in_cons; case: eqPsym => // <-; rewrite s'y.
+by rewrite in_cons; case: eqVneq => // <-; rewrite s'y.
 Qed.
 
 Lemma filter_pred1_uniq s x : uniq s -> x \in s -> filter (pred1 x) s = [:: x].
@@ -1303,7 +1303,7 @@ Lemma rot_to s x : x \in s -> rot_to_spec s x.
 Proof.
 move=> s_x; pose i := index x s; exists i (drop i.+1 s ++ take i s).
 rewrite -cat_cons {}/i; congr cat; elim: s s_x => //= y s IHs.
-by rewrite in_cons; case: eqPsym => // -> _; rewrite drop0.
+by rewrite in_cons; case: eqVneq => // -> _; rewrite drop0.
 Qed.
 
 End EqSeq.
@@ -2167,7 +2167,7 @@ Lemma nth_index_map s x0 x :
   {in s &, injective f} -> x \in s -> nth x0 s (index (f x) (map f s)) = x.
 Proof.
 elim: s => //= y s IHs inj_f s_x; rewrite (inj_in_eq inj_f) ?mem_head //.
-move: s_x; rewrite inE; case: eqPsym => [-> | _] //=; apply: IHs.
+move: s_x; rewrite inE; case: eqVneq => [-> | _] //=; apply: IHs.
 by apply: sub_in2 inj_f => z; apply: predU1r.
 Qed.