proposition: Lemma enum_yameval_countE ev : is_part ev -> forall y, is_yam_of_eval ev y -> count_mem y (enum_yameval ev) = 1.
proof: Proof. rewrite /enum_yameval /is_yam_of_eval; move Hn: (sumn ev) => n. elim: n ev Hn => [| n IHn] /= . move=> ev Hev /part0 H0 y. by rewrite (H0 Hev) => /andP[_ /eqP/evalseq0 ->]. move=> ev Hev Hpart [/= | y0 y] /=. by have -> : [::] == ev = false by move: Hev; case ev. move => /andP[/andP[_ Hyam] /eqP Htmp]; subst ev. rewrite count_flatten -map_comp. rewrite (eq_map (g := fun i => i == y0 : nat)); first last. move=> i /=; rewrite count_map /=. case: eqP => [Heq | /eqP/negbTE Hneq]. - subst i; rewrite (eq_count (a2 := xpred1 y)); first last. by move=> s; rewrite /= -eqseqE /= eq_refl /=. rewrite (incr_nthK (is_part_eval_yam Hyam) Hpart) IHn //=. + by move: Hev; rewrite sumn_incr_nth => /eqP; rewrite eqSS => /eqP. + exact: is_part_eval_yam. + by rewrite Hyam eq_refl. - rewrite (eq_count (a2 := pred0)); first by rewrite count_pred0. by move=> s; rewrite /= -eqseqE /= Hneq. rewrite sumn_count count_filter. rewrite (eq_count (a2 := xpred1 y0)); first last. move=> i /=; case eqP => //= ->. by apply: is_rem_corner_yam; rewrite /= Hpart Hyam. rewrite -sumn_count /=. rewrite sumn_pred1_iota add0n size_incr_nth. case: (ltnP y0 (size (evalseq y))) => [-> // | _]. by rewrite ltnSn leq0n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition