proposition: Lemma rotations_flip_impl t1 t2: (t1 \in rotations t2) -> (flip t2 \in rotations (flip t1)).
proof: Proof. elim: t2 t1 => // l IHl r IHr t2. move/rotationP => [a] [b] [c] [] [H1 H2]; rewrite H1 H2. - by rewrite /= inE eq_refl. - move=> H; apply/rotationP. move: H1 => [Hl Hr]; subst a; subst c => /=. exists (flip r), (flip b), (flip l); apply Or33; split => //=. exact: IHl. - move=> H; apply/rotationP. move: H1 => [Hl Hr]; subst a; subst b => /=. exists (flip c), (flip r), (flip l); apply Or32; split => //=. exact: IHr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype