proposition: Lemma mesymSS (R : ringType) n k : 's_(n.+1, k.+1) = mw 's_(n, k.+1) + mw 's_(n, k) * 'X_(ord_max) :> {mpoly R[n.+1]}.
proof: Proof. rewrite /mesym -big_set /= union_S big_set. rewrite bigU ?disjoint_S //=; congr (_ + _). + rewrite big_imset /=; last by move=> ?? _ _; apply/inj_swiden. rewrite big_set /= raddf_sum /=; apply/eq_bigr=> h _. rewrite !mprodXE mwidenX; congr 'X_[_]; apply/mnmP=> j. rewrite mnmwiden_sum !mnm_sumE big_imset //=; last first. by move=> ?? _ _; apply/inj_widen. by apply/eq_bigr=> i _; rewrite mnmwiden1. + rewrite big_imset /=; last by move=> t1 t2 _ _; apply/inj_mDswiden. rewrite big_set /= raddf_sum /= mulr_suml; apply/eq_bigr=> h _. rewrite !mprodXE mwidenX -mpolyXD; congr 'X_[_]. rewrite (big_setD1 ord_max) /= ?in_setU1 ?eqxx //=. rewrite addmC setU1K //= ?mnmwiden_sum ?big_imset /=. by congr (_ + _)%MM; apply/eq_bigr=> i _; rewrite mnmwiden1. by move=> ?? _ _; apply/inj_widen. apply/negP; case/imsetP=> /= x _ /eqP. by rewrite eqE /= eq_sym ltn_eqF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg