diff options
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. |