proposition: Lemma split_recabK (s : {set 'I_(size (to_word (t0 :: t)))}) : s = (lsh_rec @: lsplit_rec s) :|: (rsh_rec @: rsplit_rec s).
proof: Proof. Proof using. rewrite /lsplit_rec /rsplit_rec /lsh_rec /rsh_rec. apply/setP/subset_eqP/andP; split; apply/subsetP=> i Hi. - apply/setUP; rewrite -(cast_ordKV size_to_word_cons i) !imset_comp !mem_cast. have:= splitK (cast_ord (esym size_to_word_cons) i). case: fintype.splitP => j Hj; rewrite /unsplit => Hinj. + left; apply/imsetP; exists j => /=; last by rewrite Hinj. by rewrite inE /= Hinj /cast_cons cast_ordKV. + right; apply/imsetP; exists j => /=; last by rewrite Hinj. by rewrite inE /= Hinj /cast_cons cast_ordKV. - 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