proposition: Lemma fdeg_prod (T : Type) r P (F : T -> fmonom I) : fdeg (\big[mmul/1%M]_(x <- r | P x) (F x)) = (\sum_(x <- r | P x) (fdeg (F x)))%N.
proof: Proof. by apply/big_morph; [apply/fdegM|apply/fdeg1]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap