proposition: Lemma coef0M {R : ringType} (p q : {poly R}) : (p * q)`_0 = p`_0 * q`_0.
proof: Proof. by rewrite coefM big_ord1. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)