proposition: Lemma mcoeff_alt_SchurE d (la mu : 'P_d) : size la <= n -> size mu <= n -> ('a_rho * Schur n0 R la)@_(mpart mu + rho) = (la == mu)%:R.
proof: Proof. move=> Hszla Hszmu; rewrite (alt_SchurE Hszla). have sorted_mpart_rho (nu : 'P_d) : sorted gtn ((mpart nu) + rho)%MM. apply/(sorted_strictP 0%N) => // i j. rewrite size_tuple => /andP[Hij Hj]; have Hi := ltn_trans Hij Hj. rewrite -[i]/((Ordinal Hi) : nat) -mnm_nth. rewrite -[j]/((Ordinal Hj) : nat) -mnm_nth /=. rewrite !mnmE /= /mpart. have : n - 1 - j < n - 1 - i. apply ltn_sub2l => //; apply (leq_trans Hij). by move: Hj; case n => // m; rewrite ltnS subn1 /=. case: (leqP (size nu) n) => _; rewrite !mnmE ?add0n //=. rewrite -addnS; apply leq_add. have [_] := is_part_ijP _ (intpartnP nu); apply. exact: ltnW. have : perm_eq (mpart la + rho)%MM (mpart mu + rho)%MM = (la == mu). apply/idP/eqP => [Hperm | -> //]. suff : (mpart la + rho)%MM = (mpart mu + rho)%MM. move/eqP; rewrite eqm_add2r => /eqP/(congr1 (@partm n))/(congr1 pval). by rewrite !mpartK //; apply: val_inj. apply val_inj; apply val_inj => /=. exact: (irr_sorted_eq _ _ (sorted_mpart_rho la) (sorted_mpart_rho mu) (perm_mem Hperm)). case: eqP => [-> |] _. - apply mcoeff_alt. exact: (sorted_uniq _ _ (sorted_mpart_rho mu)). - rewrite /alternpol linear_sum => Hperm /=. rewrite big1 // => s _. rewrite linearZ /= msymX mcoeffX. case: eqP => [Habs |]; last by rewrite mulr0. exfalso. move: Hperm => /tuple_permP; apply. rewrite -{1}Habs; exists s; congr tval; apply eq_from_tnth => i. by rewrite -mnm_tnth !tnth_mktuple permK. 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