proposition: Lemma is_part_sortedE sh : (is_part sh) = (sorted geq sh) && (0 \notin sh).
proof: Proof. apply/idP/andP => [Hpart|]. - split. + apply/(sortedP 0) => i _. by move: Hpart=> /is_partP[_]; apply. + exact: notin0_part. - move=> [/(sortedP 0) Hsort Hnotin]. apply/is_partP; split => [| i]. + case: sh Hnotin {Hsort} => [// | s0 sh]. by apply contra => /= => /eqP <-; apply: mem_last. + case: (ltnP i.+1 (size sh)) => Hsz; first exact: Hsort. by rewrite (nth_default _ Hsz). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype