proposition: Lemma intpart_of_monP m : mnmwgt m = d -> is_part_of_n d (intpart_of_mon m).
proof: Proof. Proof using. rewrite /mnmwgt => H. rewrite /= is_part_sortedE; apply/and3P; split. - rewrite /intpart_of_mon sumn_rev sumn_flatten -[X in _ == X]H. rewrite sumnE big_map big_tuple. apply/eqP/eq_bigr => /= i _. by rewrite sumnE tnth_mktuple big_nseq iter_addn_0 mulnC. - rewrite /intpart_of_mon /= rev_sorted. apply/(sorted2P 0%N) => //=; first exact: leq_trans. move=> i j; rewrite !nth_flatten. rewrite size_flatten. have -> : shape [seq nseq (m i0) i0.+1 | i0 : 'I_n] = m. rewrite /shape -map_comp (tuple_map_ord m) /=. apply eq_map => k /=. by rewrite size_nseq. move=> /andP[Hij Hjm]; have Him := leq_ltn_trans Hij Hjm. have:= reshape_indexP Hjm; have:= reshape_offsetP Hjm. have:= reshape_indexP Him; have:= reshape_offsetP Him. rewrite size_tuple => Hc1 Hr1 Hc2 Hr2. do 2 (rewrite (nth_map ord0); last by rewrite size_enum_ord). rewrite !(mnm_nth 0) !nth_nseq !nth_enum_ord //= {Hr1 Hr2}. rewrite {}Hc1 {}Hc2 ltnS; move: Hij. by rewrite (reshape_leq m) => /orP[/ltnW | /andP[/eqP->]]. - rewrite /intpart_of_mon; rewrite mem_rev; apply/flatten_mapP => /= [[s _]]. by move=> /nseqP[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg matrix vector ssrnum algC archimedean) mathcomp(fingroup perm) mathcomp(ssrcomplements freeg mpoly) tools sorted ordtype permuted partition permcent antisym Schur_mpoly Schur_altdef sympoly