proposition: Lemma colpartn_bot sh : (colpartn d <= sh :> 'PLexi)%O.
proof: Proof. rewrite leEintpartnlexi leEseqlexi. case: sh; case: d => [|n] sh Hsh; first by rewrite intpartn0 /= rowpartn0E. rewrite /= colpartnE. move: Hsh => /andP[Hsum Hpart]; have := part_head_non0 Hpart. case: sh Hsum Hpart => //= s0 sh Hsum /andP[Hhead Hpart]. rewrite !leEnat -lt0n => Hs0; rewrite Hs0 /=; case: leqP => //= les01. have {les01}Hs0 : s0 = 1 by apply anti_leq; rewrite Hs0 les01. subst s0; suff -> : sh = nseq n 1 by apply: Order.SeqLexiOrder.refl. move: Hsum; rewrite add1n eqSS => /eqP <-. exact: (part_nseq1P Hpart Hhead). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype