proposition: Lemma ext_tabK (t : T) : eqeval t s -> res_tab (ext_tab t) = t.
proof: Proof. move=> Hev. apply val_inj => /=; rewrite -[RHS]to_wordK -[LHS]to_wordK /res_tab. by rewrite filter_ext_tab //= insubT; first case t. 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