proposition: Lemma size_conj_part sh : is_part sh -> size (conj_part sh) = head 0 sh.
proof: Proof. elim: sh => //= s0 [| s1 sh] IHsh /= /andP[Hhead {}/IHsh] /= Hrec. - by rewrite size_nseq. - by move: Hhead; rewrite -{1}Hrec => /size_incr_first_n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype