proposition: Lemma fgmulUU c1 c2 k1 k2 : fgmul << c1 *g k1 >> << c2 *g k2 >> = << c1 * c2 *g k1 * k2 >>.
proof: Proof. by rewrite (fgmulrw msuppU_le msuppU_le) !big_seq_fset1 !mcoeffUU. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap