proposition: Lemma rot_is_rot : rot = rotations.
proof: Proof. apply/setP=> r; apply/idP/idP => [|/rotations_is_rot] /[!inE]// h. have -> : r = r1 ^+ (r c0) by apply: rot_eq_c0; rewrite // -rot_r1. have e2: 2 = r2 c0 by rewrite permE /=. have e3: 3 = r3 c0 by rewrite permE /=. case (r c0); do 4?[case] => // ?; rewrite ?(expg1, eqxx, orbT) //. by rewrite [nat_of_ord _]/= e2 -rot_r1 ?(eqxx, orbT, rotations_is_rot, inE). by rewrite [nat_of_ord _]/= e3 -rot_r1 ?(eqxx, orbT, rotations_is_rot, inE). 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)