From 18edd0a87f8cc8bfd3a7c7aaaafa3d2cfdf5d165 Mon Sep 17 00:00:00 2001
From: Christian Doczkal
Date: Tue, 5 May 2020 19:50:42 +0200
Subject: cardinality lemmas for #|A| <= 1 and n <= #|A|

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

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

diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 920f393..b202dd0 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -2008,6 +2008,9 @@ 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.
+
 End Subseq.
 
 Prenex Implicits subseq.
-- 
cgit v1.2.3