proposition: Lemma group_set_iso3 : group_set iso3.
proof: Proof. apply/group_setP; split. by apply/is_iso3P => fi; rewrite -!permM mulg1 mul1g. move=> x1 y; rewrite /iso3 !inE /= /is_iso3. rewrite /is_iso3b. rewrite -mulgA. move/eqP => hx1; move/eqP => hy. rewrite hy !mulgA. by rewrite -hx1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset fingroup) mathcomp(action perm primitive_action)