proposition: Lemma is_part_consK l0 sh : is_part (l0 :: sh) -> is_part sh.
proof: Proof. by move=> /= /andP[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype