proposition: Lemma intpart_sorted (p : intpart) : sorted geq p.
proof: Proof. by have:= intpartP p; rewrite is_part_sortedE => /andP[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype