proposition: Lemma is_part_ijP sh : reflect (last 1 sh != 0 /\ forall i j, i <= j -> (nth 0 sh i) >= nth 0 sh j) (is_part sh).
proof: Proof. apply: (iffP idP) => [/is_partP[H0 H] | [H0 H]]. - split=> [| i {H0} j /subnKC <-]; first exact H0. elim: (j - i) => [|n IHn] {j}; first by rewrite addn0. rewrite addnS. exact: (leq_trans (H _) IHn). - by apply/is_partP; split => [| {H0} i]; [exact H0 | exact: H]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype