proposition: Lemma part_of_comp_subproof n (c : intcompn n) : is_part_of_n n (sort geq c).
proof: Proof. rewrite /is_part_of_n /= sumn_sort intcompn_sumn eq_refl /=. rewrite is_part_sortedE; apply/andP; split. - apply sort_sorted => x y; exact: leq_total. - by rewrite mem_sort -/(is_comp c). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype