proposition: Lemma enumIsize_to_word : enum 'I_(size (to_word (t0 :: t))) = map lsh_rec (enum 'I_(size (to_word t))) ++ map rsh_rec (enum 'I_(size t0)).
proof: Proof. Proof using. rewrite /rsh_rec /lsh_rec (enum_cast_ord size_to_word_cons). rewrite !map_comp /cast_cons -map_cat; congr (map (cast_ord size_to_word_cons) _). by rewrite map_id enumIMN. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype