proposition: Lemma partdom_rowpartn sh : (sh <= rowpartn d)%O.
proof: Proof. apply/partdomP. case: d sh => [|d1] sh; first by rewrite /= !val_intpartn0. case=> [|i] /=; rewrite ?take0 ?addn0 //. rewrite rowpartnSE /= addn0 -{2}(sumn_intpartn sh). by rewrite -{2}(cat_take_drop i.+1 sh) sumn_cat leq_addr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype