proposition: Lemma vctleq_rotation t1 t2 : right_sizes t1 <=V right_sizes t2 -> t1 != t2 -> exists t, t \in rotations t1 /\ right_sizes t <=V right_sizes t2.
proof: Proof. move=> Hvctleq Huv. have/vctleqP:= Hvctleq => [] [Hsz Hleq]. have Hneq : exists i, nth 0 (right_sizes t1) i < nth 0 (right_sizes t2) i. have {Huv} Hneq : (right_sizes t1) != (right_sizes t2). move: Huv; apply contra => /eqP/(congr1 from_vct). by rewrite !right_sizesK => ->. move: Hsz Hneq Hleq {Hvctleq}. elim: (right_sizes t1) (right_sizes t2) => {t1 t2} [| u0 u IHu] [| v0 v] //=. move/eq_add_S => Hsz; rewrite eqseq_cons negb_and => /orP[] Hneq Hleq. - exists 0; rewrite /= ltn_neqAle Hneq /=. exact: (Hleq 0). - have {}Hleq i : nth 0 u i <= nth 0 v i by apply: Hleq i.+1. have [i Hi] := IHu _ Hsz Hneq Hleq. by exists i.+1. case/ex_minnP: Hneq => i. set v0 := nth 0 (right_sizes t1) i. set w0 := nth 0 (right_sizes t2) i => H0. have Hi : i < size (right_sizes t1). move: H0; apply contraLR; rewrite -!ltnNge !ltnS /v0 /w0 => H. by rewrite nth_default; last by rewrite -Hsz. pose u := take i (right_sizes t1). pose v := drop i.+1 (right_sizes t1). pose w := drop i.+1 (right_sizes t2) => Hmin. have Hv : right_sizes t1 = u ++ v0 :: v. rewrite /u /v -{1}(cat_take_drop i (right_sizes t1)); congr (_ ++ _). rewrite -add1n -drop_drop drop1. have -> : v0 = head 0 (drop i (right_sizes t1)). by rewrite -nth0 nth_drop addn0. apply/esym/cons_head_behead. by apply/eqP/nilP; rewrite /nilp size_drop subn_eq0 -ltnNge. have {Hmin} Hw : right_sizes t2 = u ++ w0 :: w. rewrite /u /v /w -{1}(cat_take_drop i (right_sizes t2)); congr (_ ++ _). - apply (eq_from_nth (x0 := 0)); rewrite !size_take -Hsz Hi //. move=> j Hj; rewrite !nth_take -?hsz //. apply anti_leq; rewrite Hleq andbT. move: Hj; apply contraLR; rewrite -leqNgt -ltnNge. exact: Hmin. - rewrite -add1n -drop_drop drop1. have -> : w0 = head 0 (drop i (right_sizes t2)). by rewrite -nth0 nth_drop addn0. apply/esym/cons_head_behead. by apply/eqP/nilP; rewrite /nilp size_drop subn_eq0 -ltnNge -Hsz. move: Hvctleq (right_sizesP t1) (right_sizesP t2). rewrite -{3}(right_sizesK t1); rewrite Hv Hw => Hvctleq Htamv Htamw. exists (from_vct (u ++ (nth 0 v v0 + v0).+1 :: v)). split; first exact: rotations_add_bounded Htamv Htamw Hvctleq H0. have Htam0 := Tamari_add_bounded Htamv Htamw Hvctleq H0. rewrite (from_vctK Htam0); apply/vctleqP. split => [|j]; first by rewrite -Hw -Hsz Hv !size_cat. have Hieq : i = size u by rewrite /u size_take Hi. case: (ltngtP j i) => Hj. + by rewrite !nth_cat -Hieq Hj. + move/(_ j): Hleq; rewrite Hv Hw => /=. rewrite !nth_cat -Hieq [j < i]ltnNge (ltnW Hj) /=. move: Hj; rewrite -subn_gt0. by case: (j - i). + subst j. rewrite Hieq !nth_cat ltnn subnn /=. exact: Tamari_add_min Htamw Hvctleq H0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype