proposition: Lemma rotations_vctleq_impl t1 t2 : t1 \in rotations t2 -> right_sizes t2 <=V right_sizes t1.
proof: Proof. move=> Hrot; apply/vctleqP. split; first by rewrite !size_right_sizes (size_rotations Hrot). elim: t2 t1 Hrot => [//|l IHl r IHr] t2. move/rotationP => [a] [b] [c] [] [H1 H2]. - rewrite /= {IHl IHr}; subst t2 => /=. move: H1 => [Hl Hr]; subst l r => /=. rewrite -!catA !cat_cons => i. rewrite !nth_cat; case: ltnP => // _. by case: (i - _) => //=; rewrite add1n addSnnS leq_addr. - move: H1 => [Ha Hc]; subst a; subst c; subst t2 => Hrot. have:= IHl _ Hrot => {IHl IHr} Hrec i /=. rewrite !nth_cat !size_right_sizes (size_rotations Hrot). by case: ltnP. - move: H1 => [Ha Hc]; subst a; subst b; subst t2 => Hrot. have:= IHr _ Hrot => {IHl IHr} Hrec i /=. rewrite !nth_cat !size_right_sizes (size_rotations Hrot). case: ltnP => // _. by case: (i - _) => //=; rewrite add1n addSnnS leq_addr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype