proposition: Lemma le_Young_sumn: {homo (fun x : 'YL => sumn x) : x y / (x <= y)%O }.
proof: Proof. by move=> sh1 sh2; rewrite le_YoungE; exact: sumn_included. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype