proposition: Lemma yamtab_rows_dominate innev row : forall res shape, (res, shape) \in yamtab_rows innev row -> dominate res row.
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} /dominateP[Hsize Hdom]. move/mapP => [i Hi [-> _]] /=. apply/dominateP; split; first by rewrite ltnS. case=> [_ /=| j]; last by rewrite /= ltnS; apply Hdom. move: Hi; rewrite /one_letter_choices mem_filter mem_iota /= => /and3P[_]. by rewrite ltEnat. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule