proposition: Lemma extsubsm n (w : n.-tuple Alph) (P : pred 'I_n) : subseq (extractpred w P) w.
proof: Proof. Proof using. suff -> /= : tval w = mask [seq predT i | i <- enum 'I_n] w by rewrite -extractmaskE; apply: extsubsIm. rewrite (_ : map _ _ = nseq n true); first last. apply: (eq_from_nth (x0 := false)). by rewrite size_nseq size_map size_enum_ord. move=> i; rewrite size_map size_enum_ord => Hi. rewrite nth_nseq Hi nth_map => //=; last by rewrite size_enum_ord. by move: Hi; case n => [// | n0]; apply/Ordinal. by rewrite mask_true //= size_tuple. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype