From 47831fdfcc1aa313b722232cebde2d3607f2e9b2 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 19 Jul 2018 17:11:59 +0200
Subject: last_eq for exhaustivity

---
 mathcomp/ssreflect/seq.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 4bc704a..8938ac5 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -992,6 +992,9 @@ Proof. by move=> s0x; rewrite -(cat_take_drop n0 s) mem_cat /= s0x. Qed.
 Lemma mem_drop s x : x \in drop n0 s -> x \in s.
 Proof. by move=> s0'x; rewrite -(cat_take_drop n0 s) mem_cat /= s0'x orbT. Qed.
 
+Lemma last_eq s z x y : x != y -> z != y -> (last x s == y) = (last z s == y).
+Proof. by move=> /negPf xz /negPf yz; case: s => [|t s]//; rewrite xz yz. Qed.
+
 Section Filters.
 
 Variable a : pred T.
-- 
cgit v1.2.3