proposition: Theorem alt_SchurE d (la : 'P_d) : size la <= n -> 'a_rho * 's_[la] = 'a_(mpart la + rho).
proof: Proof. Proof using . suff {d la} H : forall b d, d <= b -> forall (la : 'P_d), size la <= n -> 'a_rho * 's_[la] = 'a_(mpart la + rho) by apply: H. elim=> [|b IHb] d Hd la. move: Hd; rewrite leqn0 => /eqP Hd; subst d. rewrite Schur0 mulr1 -{1}(add0m rho)=> _; congr 'a_(_ + rho). by rewrite val_intpartn0 /mpart /= mnmP => i; rewrite !mnmE /=. case: (leqP d b) => Hdb; first exact: (IHb _ Hdb). have {Hdb}Hd : d = b.+1 by apply anti_leq; rewrite Hd Hdb. elim/(@finord_wf _ 'PLexi_d) : la => la IHla Hszla. pose k := head 1%N (conj_intpartn la). pose p1 := behead (conj_intpartn la); pose d1 := sumn p1. have Hk : (d = d1 + k)%N. have:= sumn_intpartn (conj_intpartn la). rewrite /d1 /k /p1 /=. by case: (conj_part la) => [| [//= | c0] c] /=; rewrite Hd // addnC. have Hd1 : d1 <= b. rewrite -ltnS -Hd Hk. have:= part_head_non0 (intpartnP (conj_intpartn la)). rewrite -/k; case k => //= k' _. by rewrite addnS ltnS; exact: leq_addr. have p1P : is_part_of_n d1 p1 by rewrite /= /d1 eq_refl is_part_behead. pose mu := IntPartN p1P. have Hszmu : size (conj_intpartn mu) <= n. rewrite size_conj_part //. apply: (leq_trans _ Hszla); rewrite /= /p1. have := size_conj_part (intpartnP (conj_intpartn la)). rewrite conj_partK // => ->. have:= (intpartnP (conj_intpartn la)) => /=. by case: (conj_part la) => [| c0 [| c1 c]] //= /andP[]. have := alt_mpart_syme R k Hszmu. rewrite -(IHb _ Hd1 (conj_intpartn mu) Hszmu) {IHb Hszmu Hd1}. rewrite -mulrA mesym_SchurE Pieri_colpartn. rewrite (bigID (fun P0 : 'P_(d1 + k) => (size P0 <= n))) /= addrC. rewrite big1 ?add0r; first last. by move=> i /andP[_]; rewrite -ltnNge; exact: Schur_oversize. rewrite mulr_sumr. pose la' := cast_intpartn Hk la. rewrite (bigID (pred1 la')) [X in _ = X](bigID (pred1 la')) /=. set prd := BIG_P. have Hprd : prd =1 pred1 la'. rewrite {}/prd => nu /=. case: eqP => [-> | _]; rewrite ?andbT ?andbF // {nu}. rewrite cast_intpartnE {la' mu d1 Hk p1P} Hszla andbT /p1 /=. exact: vb_strip_rem_col0. rewrite !(eq_bigl _ _ Hprd) {Hprd prd} /= !big_pred1_eq cast_intpartnE. set A := (X in _ + X); set B := (X in _ = _ + X). suff -> : A = B by move=> /addIr <-{A B}; rewrite Schur_cast. apply eq_bigr => {A B} nu /andP[/andP[Hstrip Hsznu] Hnu]. pose nu' := cast_intpartn (esym Hk) nu. have Hlexi : (val nu' < la :> seqlexi _)%O. rewrite cast_intpartnE /= {nu'}. rewrite lt_neqAle; apply/andP; split. move: Hnu; apply contra => /eqP H. by apply/eqP; apply val_inj; rewrite cast_intpartnE. rewrite {Hnu Hsznu la'}. have /= -> : val la = incr_first_n (conj_part p1) k. move: Hk; rewrite /d1 /p1 /= -{2}(conj_intpartnK la) /=. rewrite -{1}(sumn_intpartn (conj_intpartn la)) /=. case: (conj_part la) => [//= | p0 p] /=; first by rewrite add0n => <-. rewrite addnC -{2}(addKn (sumn p) k) => <-. by rewrite addKn. have:= intpartnP (conj_intpartn mu). have /= {Hk p1P mu} := sumn_intpartn (conj_intpartn mu). exact: vb_strip_lexi. have Hsznu' : size nu' <= n by rewrite cast_intpartnE. have := IHla nu' Hlexi Hsznu'. rewrite Schur_cast => ->. by rewrite cast_intpartnE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(mpoly) tools combclass ordtype sorted partition tableau skewpart skewtab antisym Schur_mpoly freeSchur therule std stdtab unitriginv presentSn