proposition: Lemma set_mulgA : associative set_mulg.
proof: Proof. move=> A B C; apply/setP=> y. apply/imset2P/imset2P=> [[x1 z Ax1 /imset2P[x2 x3 Bx2 Cx3 ->] ->]| [z x3]]. by exists (x1 * x2) x3; rewrite ?mulgA //; apply/imset2P; exists x1 x2. case/imset2P=> x1 x2 Ax1 Bx2 -> Cx3 ->. by exists x1 (x2 * x3); rewrite ?mulgA //; apply/imset2P; exists x2 x3. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)