fact: Fixpoint conj_part sh := if sh is s0 :: sh then incr_first_n (conj_part sh) s0 else [::].
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype