proposition: Lemma enum_compn_countE n : forall s, is_comp_of_n n s -> count_mem s (enum_compn n) = 1.
proof: Proof. rewrite /is_comp_of_n /is_comp /enum_compn. elim: n {1 3 5}n (leqnn n) => [|aux IHaux] n /=. rewrite leqn0 => /eqP-> s. rewrite andbC => /andP[/comp0 H /eqP {}/H->]. by rewrite eq_refl. move=> Hn [|s0 s] /andP[/= ]; first by move=> /eqP<-. rewrite negb_or => Hsum /andP[s0neq0 Hs]. have /negbTE -> : n != 0. move: s0neq0; apply contra => /eqP Hn0. by move: Hsum; rewrite Hn0 addn_eq0 => /andP[/eqP->]. rewrite count_flatten -map_comp. rewrite (eq_map (g := fun i => i == s0 : nat)); first last. move=> /= i; rewrite count_map /=. case: (i =P s0) => [Heq | /eqP/negbTE Hneq]. - subst s0; rewrite (eq_count (a2 := xpred1 s)); first last. by move=> x; rewrite /= -eqseqE /= eq_refl /=. rewrite {}IHaux //=. + rewrite leq_subLR; apply (leq_trans Hn). case: i s0neq0 {Hsum} => // i _. by rewrite addSnnS; apply leq_addl. + by rewrite Hs andbT -(eqP Hsum) addKn. - rewrite (eq_count (a2 := pred0)); first by rewrite count_pred0. by move=> t; rewrite /= -eqseqE /= Hneq. rewrite sumn_pred1_iota add1n ltnS -(eqP Hsum) leq_addr andbT. by rewrite lt0n eq_sym s0neq0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype