From eac1d28204c93f082771dedb90fc5a1edec6e6f8 Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Tue, 28 May 2019 22:57:38 +0300
Subject: Add eqsP view to destruct not only x == y, but also y == x

---
 mathcomp/ssreflect/eqtype.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'mathcomp/ssreflect/eqtype.v')

diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 3fbc110..895a86e 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -196,6 +196,15 @@ 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.
+
+Lemma eqsP (T : eqType) (x y : T) : eq_xor_neq_sym x y (y == x) (x == y).
+Proof. by rewrite eq_sym; case: eqP; constructor. Qed.
+
+Arguments eqsP {T x y}.
+
 Section Contrapositives.
 
 Variables (T1 T2 : eqType).
-- 
cgit v1.2.3