proposition: Lemma mcoeff1g_is_multiplicative : multiplicative (mcoeff 1%M : {malg R[K]} -> R).
proof: Proof. split=> [g1 g2|]; rewrite ?malgCK //; pose_big_fset K E. have E1: 1%M \in E by rewrite -fsub1set. rewrite (@malgMEw E E) // (big_fsetD1 1%M) //=. 2: by close. rewrite (big_fsetD1 1%M) //= mulm1 2!mcoeffD mcoeffUU. rewrite ![\sum_(i <- E `\ 1%M) _]big_seq. rewrite !raddf_sum !big1 ?addr0 //= => k; rewrite in_fsetD1 => /andP [ne1_k _]. rewrite raddf_sum big1 ?mcoeff0 //= => k'; rewrite mcoeffU. by case: eqP=> // /eqP /unitmP []; rewrite (negbTE ne1_k). by rewrite mcoeffU mul1m (negbTE ne1_k). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap