proposition: Lemma fgscaleAl c g1 g2 : c *: (g1 * g2) = (c *: g1) * g2.
proof: Proof. by rewrite -!mul_malgC mulrA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap