proposition: Lemma extrsplit s : extract W (rsplit s) = extract [tuple of V ++ W] (s :&: [set i : 'I_(M+N)| i >= M]).
proof: Proof. Proof using. rewrite /= !extractmaskE enumIMN map_cat. rewrite mask_cat; last by rewrite 2!size_map size_enum_ord size_tuple. rewrite (_ : map _ (map lsh _) = nseq M false); first last. rewrite -map_comp. apply: (@eq_from_nth _ false); first by rewrite size_map size_enum_ord size_nseq. move => i; rewrite size_map size_enum_ord => Hi. rewrite nth_nseq Hi /= (nth_map (Ordinal Hi)) /=; last by rewrite size_enum_ord. by rewrite inE inE /= (nth_enum_ord _ Hi) leqNgt Hi /= andbF. rewrite mask_false cat0s -[in RHS]map_comp; congr (mask _ W). apply: eq_map => i /=; rewrite inE in_setI. suff -> : rsh i \in [set i0 : 'I_(M+N) | M <= i0] by rewrite andbT. by rewrite inE /=; exact: leq_addr. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype