proposition: Theorem alt_mpart_syme d (la : 'P_d) k : size la <= n -> ('a_(mpart la + rho) * 'e_k = \sum_(mu : 'P_(d + k) | vb_strip la mu && (size mu <= n)) 'a_(mpart mu + rho))%R.
proof: Proof. Proof using . rewrite alt_syme => Hszla. rewrite (bigID (hasincr la)) /=. rewrite big1 ?add0r; last by move=> i /andP[_ /hasincr0]. under eq_bigr => i /andP[/add_mesymE /[apply] <- //]. rewrite (reindex_onto _ _ (add_mesymK Hszla)). apply eq_bigl => S; rewrite inE -andbA. apply/idP/and3P => [H | [Hstrip Hszle /eqP HS]]. - split. + apply/(vb_stripP (intpartnP _) (intpartnP _)) => i /=. rewrite Hszla H /= nth_rem_trail0. case: (ssrnat.ltnP i n) => Hi; first last. rewrite !nth_default //; first last. - exact: leq_trans Hszla Hi. - by rewrite size_map size_enum_ord. have H0 : 0 < n by apply: (leq_ltn_trans _ Hi). rewrite /mpart Hszla /= (nth_map (Ordinal H0)) ?size_enum_ord // !mnmE. rewrite (nth_enum_ord (Ordinal H0) Hi). by case: (_ \in _); rewrite ?addn0 ?addn1 leqnn ltnW. + rewrite /add_mesym /= Hszla H /=. apply (leq_trans (size_rem_trail0 _)). by rewrite size_map size_enum_ord. + rewrite /setdiff; apply/eqP/setP => i. rewrite inE /= Hszla H /= nth_rem_trail0. have H0 : 0 < n by apply: (leq_ltn_trans _ (ltn_ord i)). rewrite (nth_map (Ordinal H0)); last by rewrite size_enum_ord. rewrite /mpart Hszla nth_ord_enum /= (mnm_nth 0) /= mnmE. rewrite (nth_map (Ordinal H0)); last by rewrite size_enum_ord. rewrite nth_ord_enum. by case: (i \in S); rewrite ?addn0 ?addn1 ?ltnSn ?ltnn. - rewrite -HS card_setdiff // eq_refl andTb. exact: nohasincr_setdiff. 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