proposition: Lemma cutcover (p : {set {set 'I_(M + N)}}) : cover p = lsh @: (cover (lsplit @: p)) :|: rsh @: (cover (rsplit @: p)).
proof: Proof. Proof using. rewrite /cover /=. apply/setP/subset_eqP/andP; split; apply/subsetP=> i. - move/bigcupP=> [part Hpart Hi]. have:= splitK i; case: fintype.splitP => j Hj; rewrite /unsplit => Hinj. + rewrite -Hinj; apply/setUP; left. apply: imset_f; apply/bigcupP; exists (lsplit part); first exact: imset_f. by rewrite /= inE Hinj. + rewrite -Hinj; apply/setUP; right. apply: imset_f; apply/bigcupP; exists (rsplit part); first exact: imset_f. by rewrite /= inE Hinj. - 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