proposition: Lemma is_partP sh : reflect (last 1 sh != 0 /\ forall i, (nth 0 sh i) >= nth 0 sh i.+1) (is_part sh).
proof: Proof. apply: (iffP idP). - elim: sh => //= sh0 sh IHsh /andP[Hhead Hpart]. move/(_ Hpart) : IHsh => [Hlast Hi]. split; first by case: sh Hhead Hpart Hlast Hi => [| sh1 sh] //=; case sh0. case => [|i] /=; first by move: Hhead; case sh. exact (Hi i). - elim: sh => //= sh0 sh IHsh [Hlast Hpart]. apply/andP; split. * move: Hlast; move/(_ 0) : Hpart => /=; case sh => //=. by rewrite /head ltn_neqAle eq_sym => -> ->. * apply: IHsh; split; last by move=> i; apply: (Hpart i.+1). by move: Hlast; case sh. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype