proposition: Lemma yamtab_shift_is_row innev maxi sh y : is_row y -> forall res shape, (res, shape) \in yamtab_shift innev maxi sh y -> is_row res.
proof: Proof. Proof using . elim: sh innev y => [// | sh IHsh] /= innev y Hdom res shape. by rewrite mem_seq1 => /eqP[->]. move/flatten_mapP => [[rec shrec]] /(IHsh _ _ Hdom){IHsh Hdom}Hrec. move/mapP => [i Hi [-> _]]. move: Hi; rewrite /one_letter_choices mem_filter mem_iota /= add0n subn0 ltnS. move=> /andP[_]; rewrite leq_min => /andP[_]. case: rec Hrec => [// | 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