proposition: Lemma rotations_is_rot : forall r, r \in rotations -> is_rot r.
proof: Proof. move=> r Dr; apply/eqP; apply/permP => a; rewrite !inE -!orbA !permM in Dr *. by case/or4P: Dr; move/eqP->; rewrite !permE //; case: a; do 4?case. 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)