proposition: Lemma sum_symh_syme (d : nat) : d != 0%N -> \sum_(0 <= i < d.+1) (-1) ^+ i *: ('h_i * 'e_(d - i)) = 0 :> SF.
proof: Proof. move=> Hd; apply val_inj; rewrite /= rmorph_sum /=. apply mpolyP => m; rewrite linear_sum /= mcoeff0. case: (mdeg m =P d) => Hm; first last. rewrite big_nat big1 // => i /=; rewrite ltnS => Hi. rewrite linearZ /= mcoeffM big1 ?mulr0 //= => [[m1 m2] /= /eqP Hmm]. rewrite mcoeff_symh mcoeff_mesym. case: (mdeg m1 =P i) => Hm1; rewrite ?mul0r // mul1r. rewrite /mechar. case: (mdeg m2 =P (d - i)%N) => Hm2; rewrite ?mul0r //=. exfalso; move: Hm; rewrite Hmm. by rewrite mdegD Hm1 Hm2 subnKC // eq_refl. rewrite big_nat_rev /= add0n. apply/eqP; rewrite -(mulrI_eq0 _ (lreg_sign (n := d))) mulr_sumr; apply/eqP. transitivity (\sum_(0 <= i < d.+1) (-1) ^+ i * (binomial #|[set j | m j != 0%N]| i)%:R : R). apply eq_big_nat => /= i; rewrite ltnS => Hi. rewrite subSS subKn // linearZ /= mulrA; congr (_ * _). rewrite -signr_odd -[X in _ * X]signr_odd -signr_addb. by rewrite oddB // addKb signr_odd. rewrite mcoeffM. rewrite (bigID (fun k : 'XXn_m => (mechar i k.2))) /=. rewrite addrC big1 ?add0r; first last. move=> [/= m1 m2 /andP[Hmm /negbTE Hf]]. by rewrite mcoeff_mesym Hf /= mulr0. rewrite (eq_bigr (fun k : 'XXn_m => 1)); first last. move=> [/= m1 m2 /andP[/eqP H1 H2]]. rewrite mcoeff_symh mcoeff_mesym H2 /= mulr1. suff -> : mdeg m1 == (d - i)%N by []. move: Hm; rewrite {1}H1 mdegD. move: H2 => /andP[/eqP-> _] <-. by rewrite addnK. subst d; rewrite sumr_const /= -cards_draws; congr _%:R. pose f := (fun mm : 'Xn => [set j | mm j != 0%N] : {set 'I_n}). pose g := (fun S : {set 'I_n} => [multinom (i \in S : nat) | i < n]). have canfg : {in mechar i, cancel f g}. move=> m2. rewrite unfold_in /mechar /= => /andP[_ /forallP /= Hall]. rewrite {}/f {}/g /=. apply/mnmP => j; rewrite mnmE inE. case: (m2 j =P 0%N) => [-> |] //=. by move/(_ j): Hall; case: (m2 j) => [|[|k]]. rewrite -(card_in_imset (f := f \o (fun mm : 'XXn_m => bmnm mm.2))); first last. move=> /= [m1 m2] [n1 n2]. rewrite !unfold_in /= => /andP[/eqP Hmm Hm2] /andP[/eqP Hnn Hn2] /(congr1 g). rewrite !canfg // {f g canfg} => /= [] H1. congr (_ , _); apply val_inj => //=. by rewrite -(addmK m2 m1) -Hmm -(addmK n2 n1) -Hnn H1. congr #|pred_of_set _|; apply/setP => /= S; rewrite !inE !unfold_in. apply/imsetP/andP => /= [[[m1 m2]] | [/subsetP Hsubs /eqP Hs] ]. - rewrite unfold_in /= /mechar => /andP[/eqP Hmm] /andP[/eqP Hmdeg /forallP /= Hall ->{S}]. rewrite /f /= {f g canfg}; split. + apply/subsetP => j; rewrite !inE /= {2}Hmm. by apply contra; rewrite mnmDE addn_eq0 => /andP[]. + apply/eqP; rewrite -Hmdeg /mdeg [RHS]big_tuple. rewrite (bigID (mem [set j | m2 j != 0%N])) /= addnC. rewrite [X in _ = (X + _)%N]big1 ?add0n; first last. by move=> j; rewrite inE negbK -mnm_tnth => /eqP ->. rewrite -sum1_card; apply eq_bigr => j. rewrite inE -mnm_tnth. by move/(_ j): Hall; case: (m2 j) => [|[|k]]. - have : mdeg (g S) = #|S|. rewrite /mdeg [LHS]big_tuple (bigID (mem S)) /= addnC. rewrite [X in (X + _)%N]big1 ?add0n; first last. by move=> j /negbTE; rewrite tnth_mktuple => ->. under eq_bigr => j do rewrite tnth_mktuple => ->. exact: sum1_card. rewrite Hs => HmdeggS. have Hm2 : mdeg (g S) < (mdeg m).+1 by rewrite HmdeggS ltnS. pose m2 := BMultinom Hm2. have Hm2m : (m2 <= m)%MM. apply/mnm_lepP => j; rewrite /= mnmE. case: (boolP (j \in S)) => //= /Hsubs. by rewrite inE lt0n. have Hmm := submK Hm2m. have Hm1 : mdeg (m - m2) < (mdeg m).+1. by rewrite ltnS -{3}Hmm mdegD leq_addr. exists (BMultinom Hm1, m2) => /=. - rewrite unfold_in Hmm /= /mechar HmdeggS !eq_refl /=. apply/forallP => /= j; rewrite /g mnmE. by case: (j \in S). - rewrite /f /g; apply/setP => j; rewrite inE mnmE. by case: (j \in S). subst d. have : #|[set j | m j != 0%N]| <= mdeg m. rewrite /mdeg -sum1_card big_tuple. rewrite [X in _ <= X](bigID (mem [set j | m j != 0%N])) /=. rewrite [X in (_ + X)%N]big1 ?addn0; first last. by move=> i; rewrite inE negbK mnm_tnth => /eqP. by apply leq_sum => i; rewrite inE mnm_tnth lt0n. have : #|[set j | m j != 0%N]| != 0%N. move: Hd; apply contra; rewrite cards_eq0 => /eqP/setP H. rewrite mdeg_eq0; apply/eqP/mnmP => i. by have:= H i; rewrite mnmE !inE => /negbFE => /eqP ->. move: (#|[set j | m j != 0%N]|) => C HC HCd. transitivity (\sum_(i < C.+1) (-1) ^+ i * 1 ^+ (C - i) * 1 ^+ i *+ 'C(C, i) : R); first last. by rewrite -exprBn subrr expr0n (negbTE HC). rewrite big_mkord. rewrite [LHS](bigID (fun i : 'I__ => i < C.+1)) /= addrC big1 ?add0r; first last. move=> i; rewrite -leqNgt => /bin_small ->. by rewrite mulr0. under [RHS]eq_bigr do rewrite !expr1n !mulr1 -mulr_natr. exact/esym/(big_ord_widen _ (fun i => (-1) ^+ i * ('C(C, i))%:R)). 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