fact: Fixpoint is_part sh := if sh is sh0 :: sh' then (sh0 >= head 1 sh') && (is_part sh') else true.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype