proposition: Theorem syms_sympM d (la : 'P_d) m : m != 0%N -> 's[la] * 'p_m = \sum_(sh : 'P_(m + d) | ribbon la sh) (-1) ^+ (ribbon_height la sh).-1 *: 's[sh] :> SF.
proof: Proof. move=> Hm. case: (ltnP n (size la)) => szla. rewrite syms_oversize // mul0r; apply/esym/big1 => /= i. move=> /ribbon_included/includedP[/(leq_trans szla)/syms_oversize -> _]. by rewrite scaler0. rewrite (syms_sympM_oapp _ Hm). case: m Hm => // m _. rewrite (bigID (fun i : 'I_n => add_ribbon_intpartn la m i)) /=. rewrite [X in _ + X = _]big1 ?addr0; last by move=> i; case: add_ribbon_intpartn. rewrite [RHS](bigID (fun sh => size (val sh) <= n)) /=. rewrite [X in _ = _ + X]big1 ?addr0; first last => [mu /andP[_]|]. by rewrite -ltnNge => /syms_oversize ->; rewrite scaler0. have ribbon_stop_subproof (mu : 'P_(m.+1 + d)) : (if size mu <= n then (mindropeq la mu).-1 else 0%N) < n. case: (leqP (size mu) n) => // szmu. case: mindropeq (mindropeq_leq la mu) => // md /= /leq_trans; apply. by rewrite geq_max szla szmu. pose ribbon_stop mu := Ordinal (ribbon_stop_subproof mu). rewrite (reindex_omap ribbon_stop (omap fst \o (add_ribbon_intpartn la m))) /=; first last => [i|]. case Haddrib: add_ribbon_intpartn => [[res h]|]//= _. move/add_ribbon_intpartnP in Haddrib. congr Some; apply val_inj => /=. rewrite (size_add_ribbon Haddrib) geq_max szla ltn_ord /=. rewrite (ribbon_on_mindropeq (intpartnP la) _ (add_ribbon_onP Haddrib)) //. exact: (is_part_add_ribbon _ Haddrib). apply esym; apply: eq_big => mu. rewrite andbC; case leqP => Hszmu /=; first last. + case Haddrib: add_ribbon_intpartn => [[res h]|] //=; first last. move/add_ribbon_intpartnP in Haddrib. case (_ =P Some mu) => // [[Heq]]. have := size_add_ribbon Haddrib; rewrite {res Haddrib}Heq /= => Heq. by move: Hszmu; rewrite Heq leq_max 2!ltnNge szla. + apply esym; case: (boolP (ribbon la mu)) => [Hrib | Hnrib]. * have := ribbon_addE (intpartnP la) (intpartnP mu) Hrib. rewrite sumn_diff_shape ?ribbon_included // !sumn_intpartn addnK. rewrite add_ribbon_intpartnE. case Haddrib: add_ribbon_intpartn => [[res h]|]//=. by move=> [/val_inj ->]; rewrite eqxx. * case Haddrib: add_ribbon_intpartn => [[res h]|]//=. move/add_ribbon_intpartnP in Haddrib. apply/negP => /eqP[] Heq. by move: Hnrib; rewrite -{}Heq (add_ribbonP _ Haddrib). move=> /andP[Hrib ->]. have:= ribbon_addE (intpartnP la) (intpartnP mu) Hrib. rewrite sumn_diff_shape ?ribbon_included // !sumn_intpartn addnK. rewrite add_ribbon_intpartnE. by case Haddrib: add_ribbon_intpartn => [[res h]|]//= [/val_inj -> <-]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint perm fingroup tuple vector rat) mathcomp(ssrcomplements freeg mpoly monalg) sorted tools ordtype permuted partition skewpart antisym Schur_mpoly Schur_altdef sympoly homogsym