proposition: Lemma tabnat_of_ordK : {in [pred t : tabsh la | eval (to_word t) == td], cancel tabnat_of_ord tabord_of_nat }.
proof: Proof. move=> /= t; rewrite inE => /eqP Ht. apply val_inj; rewrite /= /tabord_of_nat_fun /= /tabnat_of_ord_fun /=. rewrite -Ht eq_refl. rewrite -map_comp map_id_in // => /= r Hr. rewrite -map_comp map_id_in // => /= i Hi. by apply val_inj; rewrite /= inordK. 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