proposition: Lemma one_letter_included innev mini maxi : included innev outev -> forall i, i \in one_letter_choices innev mini maxi -> included (incr_nth innev i) outev.
proof: Proof. Proof using . move=> Hincl => i. rewrite /one_letter_choices mem_filter mem_iota => /andP[/andP[_ Hnth] _]. exact: included_incr_nth_inner. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule