proposition: Lemma rotations_flip t1 t2: (t1 \in rotations t2) = (flip t2 \in rotations (flip t1)).
proof: Proof. apply/idP/idP; first exact: rotations_flip_impl. by move=> /rotations_flip_impl; rewrite !flipK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype