proposition: Lemma dhomog_XS (m : 'X_{1..n}) : 'X_[m] \mPo S \is (mnmwgt m).-homog.
proof: Proof. pose dt := [tuple (i.+1 * m i)%N | i < n]. pose mt := [tuple (mesym n R i.+1) ^+ m i | i < n]. rewrite [X in X \is _](_ : _ = \prod_(i <- mt) i); last first. rewrite comp_mpolyX (eq_bigr (tnth mt)) ?big_tuple //. by move=> i _ /=; rewrite !tnth_mktuple. rewrite [X in X.-homog](_ : _ = (\sum_(i <- dt) i)%N); last first. rewrite /mnmwgt big_tuple (eq_bigr (tnth dt)) //. by move=> i _ /=; rewrite !tnth_mktuple mulnC. apply/dhomog_prod => i; rewrite !tnth_mktuple => {mt dt}. exact/dhomogMn/dhomog_mesym. 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