diff options
| author | Cyril Cohen | 2020-06-19 04:59:41 +0200 |
|---|---|---|
| committer | GitHub | 2020-06-19 04:59:41 +0200 |
| commit | f25ef67ad2f58a30f1e700da89811b193755d84e (patch) | |
| tree | 618911dc534dec482afef6aef15d032073a59f70 /mathcomp/ssreflect/seq.v | |
| parent | 3ceb153b972cbfc23a33daa740ec31050881bfa2 (diff) | |
| parent | 7fd6f9ba051ecc7be7bd95ca3e31bb1a798598ba (diff) | |
Merge pull request #509 from chdoc/card-lemmas
Card lemmas
Diffstat (limited to 'mathcomp/ssreflect/seq.v')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 920f393..dec68a3 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -2008,6 +2008,12 @@ Proof. by rewrite -cats1 prefix_subseq. Qed. Lemma subseq_uniq s1 s2 : subseq s1 s2 -> uniq s2 -> uniq s1. Proof. by case/subseqP=> m _ -> Us2; apply: mask_uniq. Qed. +Lemma take_uniq s n : uniq s -> uniq (take n s). +Proof. exact/subseq_uniq/take_subseq. Qed. + +Lemma drop_uniq s n : uniq s -> uniq (drop n s). +Proof. exact/subseq_uniq/drop_subseq. Qed. + End Subseq. Prenex Implicits subseq. |