proposition: Lemma tabord_of_nat_subproof (t : stdtabsh la) : is_tab_of_shape la (tabord_of_nat_fun t).
proof: Proof. have /andP[Ht Hstd] := stdtabshP t. rewrite /tabord_of_nat_fun /=. rewrite shape_map_tab shape_stdtabsh eq_refl andbT. move: Hstd; rewrite /is_std size_to_word. rewrite /size_tab shape_stdtabsh sumn_intpartn => /perm_mem Hperm. rewrite -incr_tab // => /= i j. rewrite !Hperm !mem_iota /= !add0n => /leq_trans/(_ Hd) Hi /leq_trans/(_ Hd) Hj. by rewrite ltEord !ltEnat /= !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