From e093066581895bd26a60dc6b1ccc17d3f8bd3123 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 20 Mar 2019 23:38:38 +0100
Subject: missing lemma in seq.v

---
 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 f503613..19ab9d3 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -1926,6 +1926,9 @@ Qed.
 Lemma mem_rem_uniq s : uniq s -> rem s =i [predD1 s & x].
 Proof. by move/rem_filter=> -> y; rewrite mem_filter. Qed.
 
+Lemma mem_rem_uniqF s : uniq s -> x \in rem s = false.
+Proof. by move/mem_rem_uniq->; rewrite inE eqxx. Qed.
+
 End Rem.
 
 Section Map.
-- 
cgit v1.2.3