diff options
| author | Cyril Cohen | 2018-12-19 15:43:31 +0100 |
|---|---|---|
| committer | Assia Mahboubi | 2018-12-19 15:43:31 +0100 |
| commit | d86a673e1be70962504c8e44af71723c2a0d1a79 (patch) | |
| tree | d4ee3e776c5aa455e47347c0ee379c1eb829911e /mathcomp/ssreflect/seq.v | |
| parent | 91fa7b5739605e70959e9a02c43135ca55c12e0a (diff) | |
Generalizing homo-mono-morphism lemmas and extremum (#201)
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 a574710..a9cc2ac 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1842,6 +1842,12 @@ Proof. by rewrite -[s1 in subseq s1]cats0 cat_subseq ?sub0seq. Qed. Lemma suffix_subseq s1 s2 : subseq s2 (s1 ++ s2). Proof. exact: cat_subseq (sub0seq s1) _. Qed. +Lemma take_subseq s i : subseq (take i s) s. +Proof. by rewrite -[s in X in subseq _ X](cat_take_drop i) prefix_subseq. Qed. + +Lemma drop_subseq s i : subseq (drop i s) s. +Proof. by rewrite -[s in X in subseq _ X](cat_take_drop i) suffix_subseq. Qed. + Lemma mem_subseq s1 s2 : subseq s1 s2 -> {subset s1 <= s2}. Proof. by case/subseqP=> m _ -> x; apply: mem_mask. Qed. |