proposition: Lemma fgmulgDr : right_distributive fgmul +%R.
proof: Proof. move=> g g1 g2; rewrite [in RHS](fgmulrwl (fsubsetUl _ (msupp g2))). rewrite [in RHS](fgmulrwl (fsubsetUr (msupp g1) _)) (fgmulrwl (msuppD_le _ _)). rewrite -big_split /=; apply/eq_bigr => k1 _. rewrite -big_split /=; apply/eq_bigr => k2 _. by rewrite mcoeffD mulrDr monalgUD. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap