proposition: Lemma enumIMN : enum 'I_(M + N) = map lsh (enum 'I_M) ++ map rsh (enum 'I_N).
proof: Proof. Proof using. apply: (inj_map (@ord_inj (M + N))). rewrite map_cat -2!map_comp !val_enum_ord. rewrite (eq_map (g := (addn M) \o val)); last by []. by rewrite map_comp !val_enum_ord -iotaDl [M + 0]addnC iotaD. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype