proposition: Lemma mcoeff0_is_multiplicative : multiplicative (mcoeff 0%MM : {mpoly R[n]} -> R).
proof: Proof. split=> [p q|]; rewrite ?mpolyCK //. rewrite (mcoeff_poly_mul _ _ (k := 1)) ?mdeg0 //. rewrite (bigD1 (bm0, bm0)) ?simpm //=; last first. rewrite [X in _+X]big1 ?addr0 // => i /andP [] h. rewrite eqE /= !bmeqP /=; move/eqP/esym/(congr1 mdeg): h. rewrite mdegD [X in _=X]mdeg0 => /eqP; rewrite addn_eq0. by rewrite !mdeg_eq0=> /andP [/eqP->/eqP->]; rewrite !eqxx. 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