proposition: Lemma one_letter_choicesP innev mini maxi : forall i, i \in one_letter_choices innev mini maxi -> is_skew_yam innev (incr_nth innev i) [:: i].
proof: Proof. Proof using . rewrite /is_skew_yam /is_yam_of_eval => i. rewrite mem_filter mem_iota => /andP[/andP[Hcorn _] _]. move => y /andP[Hyam /eqP Hinnev]; subst innev. apply/andP; split => //=. rewrite Hyam andbT. apply is_part_incr_nth; last exact Hcorn. exact: is_part_eval_yam. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule