proposition: Lemma split_rec_cover (p : {set {set 'I_(size (to_word (t0 :: t)))}}) : cover p = lsh_rec @: (cover (lsplit_rec @: p)) :|: rsh_rec @: (cover (rsplit_rec @: p)).
proof: Proof. Proof using. rewrite /lsplit_rec /rsplit_rec /lsh_rec /rsh_rec /cover. apply/setP/subset_eqP/andP; split; apply/subsetP=> i. - move/bigcupP=> [part Hpart Hi]. rewrite -(cast_ordKV size_to_word_cons i). have:= splitK (cast_ord (esym size_to_word_cons) i). case: fintype.splitP => j Hj; rewrite /unsplit => Hinj. + rewrite -Hinj; apply/setUP; left. rewrite /cast_cons imset_comp mem_cast; apply: imset_f; apply/bigcupP. exists (lsplit_rec part); first exact: imset_f. by rewrite inE /lsh_rec /= Hinj /cast_cons cast_ordKV. + rewrite -Hinj; apply/setUP; right. rewrite /cast_cons imset_comp mem_cast; apply: imset_f; apply/bigcupP. exists (rsplit_rec part); first exact: imset_f. by rewrite inE /rsh_rec /= Hinj /cast_cons cast_ordKV. - by move/setUP => [] /imsetP[j /bigcupP[part /imsetP[prt Hprt Hcut Hj ->]]]; apply/bigcupP; exists prt => //=; move: Hj; rewrite Hcut inE. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype