proposition: Lemma mdeg_prod (T : Type) r P (F : T -> cmonom I) : mdeg (\big[mmul/1%M]_(x <- r | P x) (F x)) = (\sum_(x <- r | P x) (mdeg (F x)))%N.
proof: Proof. exact/big_morph/mdeg1/mdegM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap