proposition: Lemma rowpartn_top sh : (sh <= rowpartn d :> 'PLexi)%O.
proof: Proof. rewrite leEintpartnlexi leEseqlexi. case: sh; case: d => [|n] sh Hsh; first by rewrite intpartn0 /= rowpartn0E. rewrite /= rowpartnSE; case: sh Hsh => //= s0 sh /andP[/eqP<- /andP[_ Hpart]]. rewrite !leEnat leq_addr /=; case: leqP => //=. rewrite -{2}(addn0 s0) leq_add2l leqn0 => /eqP/(part0 Hpart) ->. by rewrite leEseqlexi. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype