proposition: Lemma extlsplit s : extract V (lsplit 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 rsh _) = nseq N 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 /= -[M in _ < M]addn0 ltn_add2l ltn0 andbF. rewrite mask_false cats0 -[in RHS]map_comp; congr (mask _ V). apply: eq_map => i /=; rewrite inE in_setI. suff -> : lsh i \in [set i0 : 'I_(M+N) | i0 < M] by rewrite andbT. by rewrite inE /=; exact: ltn_ord. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype