proposition: Lemma fgmulA : associative fgmul.
proof: Proof. move=> g1 g2 g3. rewrite [RHS](big_morph (fgmul^~ _) (fun _ _ => fgmulgDl _ _ _) (fgmul0g _)). rewrite fgmulEl1; apply/eq_bigr=> k1 _. rewrite [LHS](big_morph (fgmul _) (fun _ _ => fgmulgDr _ _ _) (fgmulg0 _)). rewrite [RHS](big_morph (fgmul^~ _) (fun _ _ => fgmulgDl _ _ _) (fgmul0g _)). apply/eq_bigr=> k2 _. rewrite [LHS](big_morph (fgmul _) (fun _ _ => fgmulgDr _ _ _) (fgmulg0 _)). by rewrite fgmulEr1; apply/eq_bigr=> k3 _; rewrite !fgmulUU mulrA mulmA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap