proposition: Lemma part_sumn_count l : is_part l -> (\sum_(i < (sumn l).+1 | val i \in l) i * (count_mem (val i) l))%N = sumn l.
proof: Proof. have [b Hb]:= ubnPleq (sumn l).+1. have {}Hb : all (gtn b) l. elim: l Hb => //= l0 l IHl H; apply/andP; split. - exact: (leq_ltn_trans (leq_addr _ _) H). - by apply IHl; exact: (leq_ltn_trans (leq_addl _ _) H). elim: l Hb => [_ _ | l0 l IHl]; first by apply big1. move=> /andP[Hb {}/IHl Hrec] Hpart. move: Hb => /= Hl0b. have /= Hl0 := part_head_non0 Hpart. move: Hpart => /andP[_] {}/Hrec Hrec. rewrite (bigD1 (Ordinal Hl0b)) /=; last by rewrite inE eq_refl. rewrite eq_refl /= mulnDr muln1 -addnA; congr (_ + _)%N. under eq_bigr => i /andP[_ /negbTE Hi]. rewrite -val_eqE /= in Hi. by rewrite eq_sym Hi add0n over. case: (boolP (l0 \in l)) => Hl0l. - rewrite -{}Hrec [RHS](bigD1 (Ordinal Hl0b)) //=; congr (_ + _)%N. apply: eq_bigl => i; congr (_ && _); rewrite inE. by case: eqP => [->|]. - rewrite (count_memPn Hl0l) muln0 add0n. rewrite -{}Hrec; apply eq_bigl => i. rewrite inE; case: (i =P l0 :> nat) => [Hi | /eqP Hil0] /=. + subst l0; rewrite (negbTE Hl0l). by apply negbTE; rewrite negbK; apply/eqP/val_inj. + by rewrite Hil0 andbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(ssrcomplements freeg mpoly) sorted tools ordtype permuted partition skewpart composition Yamanouchi std tableau stdtab skewtab permcent antisym Schur_mpoly therule Schur_altdef unitriginv