proposition: Lemma enum_compn_allP n : all (is_comp_of_n n) (enum_compn n).
proof: Proof. rewrite /is_comp_of_n /is_comp /enum_compn. elim: n {1 3 5}n (leqnn n) => [|aux IHaux] n /=. by rewrite /= leqn0 !andbT => /eqP ->. move=> Hn. case: (n =P 0) => [-> // | _]. apply/allP => /= lst /flatten_mapP[/= i]. rewrite mem_iota add1n ltnS => /andP[lt0i lein] /mapP[/= s Hs ->{lst}]. have {}/IHaux/allP/(_ s Hs)/= : n - i <= aux. rewrite leq_subLR; apply (leq_trans Hn). case: i lt0i {lein Hs} => // i _. by rewrite addSnnS; apply leq_addl. rewrite negb_or => /andP[/eqP -> ->]. rewrite subnKC // eq_refl /= andbT. by rewrite eq_sym -lt0n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype