proposition: Lemma enum_yamevalP ev: is_part ev -> all (is_yam_of_eval ev) (enum_yameval ev).
proof: Proof. move=> Hpart; apply/allP => y. rewrite /enum_yameval /is_yam_of_eval; move Hn: (sumn ev) => n. elim: n ev Hpart Hn y => [| n IHn] /= . by move=> ev Hsh /part0 H0 y; rewrite mem_seq1 H0 //= => /eqP ->. move=> ev Hpart Hev [| y0 y] /=. - have -> : [::] == ev = false by move: Hev; case ev. by move/flattenP => [ltmp /mapP[i _ ->] /mapP[]]. - move/flatten_mapP => [i]. rewrite mem_filter mem_iota add0n => /and3P[Hcorn _ Hi]. move/mapP => [x Hx [Hitmp Hxtmp]]; subst i x. have Hsum : sumn (decr_nth ev y0) = n by rewrite sumn_decr_nth //= Hev. move/(_ _ (is_part_decr_nth Hpart Hcorn) Hsum _ Hx): IHn => /andP[-> /eqP ->]. by rewrite decr_nthK //= Hpart /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition