proposition: Lemma size_leq_skew_reshape (y : seq nat) : size (RS (std (hyper_yam P1))) <= size (skew_reshape P1 P y).
proof: Proof. Proof using Hincl. rewrite -(size_map size) -/(shape (RS _)) shape_RS_std. rewrite shape_RS_yam; last by apply hyper_yamP; apply intpartnP. rewrite (evalseq_hyper_yam (intpartnP P1)). rewrite size_skew_reshape; exact: size_included. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools ordcast combclass partition skewpart Yamanouchi ordtype std tableau stdtab Schensted congr plactic Greene_inv stdplact Yam_plact skewtab shuffle Schur_mpoly freeSchur