proposition: Lemma sdprod_mulgA : associative sdprod_mul.
proof: Proof. move=> u v w; apply: val_inj; case: u => [[a x]] /=; case/setXP=> Da Rx. case: v w => [[b y]] /=; case/setXP=> Db Ry [[c z]] /=; case/setXP=> Dc Rz. by rewrite !(actMin to) // gactM ?gact_stable // !mulgA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)