proposition: Lemma coef0_prod {R : ringType} {T : Type} (ps : seq T) (F : T -> {poly R}) P : (\prod_(p <- ps | P p) F p)`_0 = \prod_(p <- ps | P p) (F p)`_0.
proof: Proof. by apply: (big_morph (fun p : {poly R} => p`_0)); [apply: coef0M | rewrite coefC eqxx]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)