From a18a03452a84e1f54716ce20accca4e16715e382 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Thu, 19 Nov 2020 18:12:26 +0900
Subject: Add `_in` lemmas for `sort`

---
 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 a0a0548..fab3fa9 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -2385,6 +2385,12 @@ Notation "[ 'seq' E : R | i : T <- s & C ]" :=
 Lemma filter_mask T a (s : seq T) : filter a s = mask (map a s) s.
 Proof. by elim: s => //= x s <-; case: (a x). Qed.
 
+Lemma all_sigP T a (s : seq T) : all a s -> {s' : seq (sig a) | map sval s' = s}.
+Proof.
+elim: s => /= [_|x s ihs /andP [ax /ihs [s' <-]]]; first by exists [::].
+by exists (exist a x ax :: s').
+Qed.
+
 Section MiscMask.
 
 Lemma leq_count_mask T (P : {pred T}) m s : count P (mask m s) <= count P s.
-- 
cgit v1.2.3