proposition: Lemma splitsetK (s : {set 'I_(M+N)}) : s = (lsh @: lsplit s) :|: (rsh @: rsplit s).
proof: Proof. Proof using. rewrite /=; apply/setP/subset_eqP/andP; split; apply/subsetP=> i Hi. - apply/setUP. have:= splitK i; case: fintype.splitP => j Hj; rewrite /unsplit => Hinj. + left; apply/imsetP; exists j => /=; last by rewrite Hinj. by rewrite inE Hinj. + right; apply/imsetP; exists j => /=; last by rewrite Hinj. by rewrite inE Hinj. - by move: Hi; rewrite inE => /orP[]; move/imsetP => [j]; rewrite inE => H ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype