proposition: Lemma tabord_of_natK : cancel tabord_of_nat tabnat_of_ord.
proof: Proof. move=> t. apply val_inj; rewrite /= /tabnat_of_ord_fun /= /tabord_of_nat_fun /=. rewrite to_word_map_tab stdtabsh_eval_to_word eq_refl. rewrite -map_comp map_id_in // => /= r Hr. rewrite -map_comp map_id_in // => /= i Hi. rewrite inordK //; apply: (leq_trans _ Hd). have : i \in to_word t. by rewrite /to_word; apply/flattenP; exists r; first rewrite mem_rev. have /andP[_] := stdtabshP t. rewrite /is_std => /perm_mem ->. rewrite mem_iota /= add0n. by rewrite size_to_word /size_tab shape_stdtabsh sumn_intpartn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(mpoly) tools combclass ordtype sorted partition tableau skewpart skewtab antisym Schur_mpoly freeSchur therule std stdtab unitriginv presentSn