proposition: Lemma lt_Young_sumn: {homo (fun x : 'YL => sumn x) : x y / (x < y)%O }.
proof: Proof. move=> sh1 sh2; rewrite !lt_neqAle => /andP[neq Hincl]. rewrite le_Young_sumn // andbT. move: neq; apply contra => /eqP/included_sumnE - /(_ (intpartP _) Hincl) Heq. exact/eqP/val_inj. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype