diff options
| author | Cyril Cohen | 2019-03-20 23:38:38 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2019-03-22 14:58:16 +0100 |
| commit | e093066581895bd26a60dc6b1ccc17d3f8bd3123 (patch) | |
| tree | e9929ee89aef9a40e366c8a472dfafb6879971c2 /mathcomp | |
| parent | 794cfe568c2b2e1eb138a8f881c330838d8a3c2d (diff) | |
missing lemma in seq.v
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 3 |
1 files changed, 3 insertions, 0 deletions
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. |