proposition: Lemma yamtab_rows_is_row innev row : forall res shape, (res, shape) \in yamtab_rows innev row -> is_row res.
proof: Proof. Proof using . elim: row innev => [| r0 tlr IHrow] /= innev res shape. by rewrite mem_seq1 => /eqP[->]. move/flatten_mapP => [[rec shrec]] /(IHrow innev) {IHrow} Hrow. move/mapP => [i Hi [-> _]] /=. move: Hi; rewrite /one_letter_choices mem_filter mem_iota /=. move => /and3P[/andP[_ Hnth] Hr0]. rewrite subSS addSn ltnS. case: (ltnP (minn (size shrec) (head (size innev) rec)) r0) => H. - move/ltnW: H; rewrite {1}/leq => /eqP ->. rewrite addn0 => /(leq_trans Hr0). by rewrite ltnn. - rewrite (subnKC H) leq_min => /andP[_]. case: rec Hrow {H} => [// | rec0 rec /= ->]. by rewrite leEnat => ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule