proposition: Lemma head_row_skew_yam innev shape l r : is_part innev -> sorted <=%O (l :: r) -> is_skew_yam innev shape (l :: r) -> l <= head (size innev) r.
proof: Proof. case: r => [| l1 r /=] Hinn Hrow Hskew. apply (is_part_incr_nth_size Hinn). move/(_ _ (hyper_yam_of_eval Hinn)): Hskew. rewrite /= /is_yam_of_eval /=. by rewrite (evalseq_hyper_yam Hinn) => /andP[] /andP[]. move: Hrow => /andP[]. by rewrite leEnat. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule