proposition: Lemma enum_compnP n s : (is_comp_of_n n s) = (s \in enum_compn n).
proof: Proof. apply/idP/idP; last by move/(allP (enum_compn_allP n)). by rewrite -has_pred1 has_count; move/enum_compn_countE ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype