proposition: Theorem rotations_right_sizesP t1 t2 : reflect (exists u v0 v, right_sizes t1 = u ++ v0 :: v /\ right_sizes t2 = u ++ (nth 0 v v0 + v0).+1 :: v) (t2 \in rotations t1).
proof: Proof. apply (iffP idP); first last. move=> [u] [v0] [v] [Ht1 Ht2]. rewrite -(right_sizesK t1) -(right_sizesK t2) Ht1 Ht2. by apply: rotations_add; rewrite -?Ht1 -?Ht2; apply: right_sizesP. have [n] := ubnPleq (size_tree t1); elim: n => [|n IHn] in t1 t2 *. by rewrite leqn0 => /LeafP ->. rewrite leq_eqVlt => /orP[/eqP Hsz Hrot|]; last by rewrite ltnS; exact: IHn. move/rotationP: Hrot Hsz => [a] [b] [c] [] [->{t1} ->{t2}] /=. - exists (right_sizes a), (size_tree b), (right_sizes b ++ size_tree c :: right_sizes c); split. + by rewrite -!catA. + by rewrite nth_cat size_right_sizes ltnn subnn nth0 /= add1n addSn addnC. - move=> {}/IHn Hrec. rewrite /= add1n addSn => /succn_inj Hsz. have: size_tree a <= n by rewrite -Hsz leq_addr. move=> {}/Hrec [u] [v0] [v] [Ha Hb]. exists u, v0, (v ++ size_tree c :: right_sizes c); split. + by rewrite Ha -!catA. + rewrite Hb nth_cat. suff -> : v0 < size v by rewrite -!catA. have := right_sizesP b; rewrite Hb => /Tamari_catr/Tamari_consP[H _ _]. exact: (leq_ltn_trans (leq_addl _ _) H). - move=> {}/IHn Hrec. rewrite /= add1n addSn => /succn_inj Hsz. have: size_tree b <= n by rewrite -Hsz leq_addl. move=> {}/Hrec [u] [v0] [v] [Hb Hc]. exists (right_sizes a ++ size_tree b :: u), v0, v; split. + by rewrite Hb -!catA. + rewrite Hc /= -!catA /=. suff -> : size_tree b = size_tree c by []. by rewrite -!size_right_sizes Hb Hc !size_cat /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype