proposition: Lemma LRyamtab_list_pad0 innev inner outer sh0 row0 : LRyamtab_list_rec innev inner outer sh0 row0 = LRyamtab_list_rec innev (pad 0 (size outer) inner) outer sh0 row0.
proof: Proof. Proof using . elim: outer innev inner sh0 row0 => [// | out0 out IHout] /= innev inner sh0 row0. congr flatten. rewrite (_ : head 0 (inner ++ nseq _ 0) = head 0 inner); last by case inner. apply eq_map => i; congr map. rewrite IHout /=; congr LRyamtab_list_rec. by case: inner; rewrite //= subn0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule