proposition: Lemma extnprod_mulgA : associative extnprod_mulg.
proof: Proof. by move=> x y z; apply/ffunP => i; rewrite !ffunE mulgA. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)