From 96efc4fa2a3b643c6c4ea19047c3e633c5af145f Mon Sep 17 00:00:00 2001
From: Christian Doczkal
Date: Sun, 7 Jun 2020 11:17:14 +0200
Subject: drop_uniq / CHANGELOG

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

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index b202dd0..dec68a3 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -2011,6 +2011,9 @@ 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.
-- 
cgit v1.2.3