proposition: Lemma fgmulgDl : left_distributive fgmul +%R.
proof: Proof. move=> g1 g2 g; rewrite [in RHS](fgmullwl (fsubsetUl _ (msupp g2))). rewrite [in RHS](fgmullwl (fsubsetUr (msupp g1) _)) (fgmullwl (msuppD_le _ _)). rewrite -big_split /=; apply/eq_bigr=> k1 _. rewrite -big_split /=; apply/eq_bigr=> k2 _. by rewrite mcoeffD mulrDl 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