proposition: Lemma coeff_symh_to_symp n (l : 'P_n) : [char R] =i pred0 -> \sum_(c : intcompn n | perm_eq l c) \Pi c = (zcard l)%:R^-1 :> R.
proof: Proof. rewrite charf0P => Hchar. case: l => l /= /andP[/eqP]. have [m/ltnW] := ubnP n; elim: m => [| m IHm] in n l *. rewrite leqn0 => /eqP-> /part0 /[apply] ->{l}. rewrite zcard_nil /=. rewrite (eq_bigl (xpred1 (rowcompn 0))); first by rewrite big_pred1_eq. move=> i; apply/idP/eqP => [Hperm | /(congr1 val)/= -> //]. by apply val_inj => /=; apply/nilP; rewrite /nilp -(perm_size Hperm). rewrite leq_eqVlt => /orP[/eqP Hm|]; last by rewrite ltnS; exact: IHm. move => Hsum Hpart. have head_intcompn (c : intcompn n) : head 0%N c < n.+1. rewrite ltnS; case: c => [[|c0 c]] //= /andP[/eqP <- _]. exact: leq_addr. pose headcomp c := Ordinal (head_intcompn c). rewrite (partition_big headcomp xpredT) //=. under eq_bigr do under eq_bigl do rewrite -val_eqE /=. rewrite (bigID (fun j => val j \in l)) /= [X in _ + X]big1 ?addr0; first last. move=> i Hi; apply big1 => [] [[|c0 c]/= _ /andP[Hperm /eqP Hhead]]; exfalso. - by move/perm_sumn: Hperm; rewrite /= Hsum Hm. - subst c0; move/perm_mem: Hperm Hi => /(_ i). by rewrite inE eq_refl /= => ->. rewrite (eq_bigr (fun i => n%:R^-1 * (zcard (rem (val i) l))%:R^-1 : R)); first last => [/= i Hi|]. have H0i := in_part_non0 Hpart Hi. have Hin : i <= n by rewrite -ltnS. rewrite (reindex (intcompn_cons H0i Hin)) /=; first last. exists (intcompn_behead H0i Hin) => c; rewrite inE => /andP[Hperm Hhead]; apply val_inj; rewrite /= ?eq_refl //. rewrite /= Hhead. case: c Hperm Hhead => [[|c0 c]] //= _. + by move/perm_sumn; rewrite /= Hsum {1}Hm. + by move=> _ /eqP ->. under eq_bigl => c do rewrite eq_refl andbT (permPl (perm_to_rem Hi)) perm_cons. under eq_bigr => c _ do rewrite intcompn_sumn subnKC // natrM invfM. rewrite -mulr_sumr IHm //. - move: H0i; case i => [/= [//|i']] _ _. by rewrite Hm subSS leq_subr. - rewrite -[LHS](addKn i). have /perm_sumn /= <- := perm_to_rem Hi. by rewrite Hsum. - move: Hpart; rewrite !is_part_sortedE => /andP[Hsort H0]. have Hrem := rem_subseq (val i) l; apply/andP; split. + exact: (subseq_sorted _ Hrem). + by move: H0; apply contra; apply (mem_subseq Hrem). rewrite {IHm} -mulr_sumr. rewrite (eq_bigr (fun i => (val i * (count_mem (val i) l))%:R / (zcard l)%:R)); first last => [i Hi|] /=. have H0i := in_part_non0 Hpart Hi. rewrite -(zcard_rem H0i Hi) [X in _ / X]natrM invfM -[LHS]mul1r !mulrA. congr (_ * _); rewrite divff // Hchar. rewrite muln_eq0 negb_or H0i /=. by move: Hi; apply contraL => /eqP H; apply/count_memPn. rewrite -mulr_suml mulrA -[RHS]mul1r; congr (_ * _). rewrite -natr_sum -Hsum part_sumn_count // mulrC divff //. by rewrite Hchar Hsum Hm. 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