proposition: Lemma mprodXnE {I} F P (m : I -> nat) (r : seq _) : \prod_(i <- r | P i) 'X_[R, F i] ^+ m i = 'X_[\sum_(i <- r | P i) (F i *+ m i)].
proof: Proof. elim/big_rec2: _ => /= [|i m' p Pi ->]. by rewrite mpolyX0. by rewrite ?(mpolyXD, mpolyXn). 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