proposition: Lemma group_set_rot : group_set rot.
proof: Proof. apply/group_setP; split; first by rewrite /rot inE /is_rot mulg1 mul1g. move=> x1 y; rewrite /rot !inE /= /is_rot; move/eqP => hx1; move/eqP => hy. by rewrite -mulgA hy !mulgA 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)