proposition: Lemma LRyamtab_list_size innev inner outer sh0 row0 : forall res, res \in LRyamtab_list_rec innev inner outer sh0 row0 -> size res = size outer.
proof: Proof. Proof using . elim: outer innev inner sh0 row0 => [// | out0 out IHout] /= innev inner sh0 row0 res. by rewrite mem_seq1 => /eqP -> /=. move=> /flatten_mapP[[rshift shrshift]]. move=> /flatten_mapP[[rrow shrrow]] /= Hrow Hshift. move=> /mapP[rec Hrec ->] {res} /=. by rewrite (IHout _ _ _ _ _ Hrec). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule