From d86a673e1be70962504c8e44af71723c2a0d1a79 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 19 Dec 2018 15:43:31 +0100
Subject: Generalizing homo-mono-morphism lemmas and extremum (#201)

---
 mathcomp/ssreflect/seq.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'mathcomp/ssreflect/seq.v')

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.
 
-- 
cgit v1.2.3