proposition: Lemma rotations_add u v0 v : u ++ v0 :: v \is a TamariVector -> u ++ (nth 0 v v0 + v0).+1 :: v \is a TamariVector -> from_vct (u ++ (nth 0 v v0 + v0).+1 :: v) \in rotations (from_vct (u ++ v0 :: v)).
proof: Proof. rewrite /from_vct; move: BinLeaf. have [n/ltnW] := ubnP (size u); elim: n => [|n IHn] in u v0 v *. by rewrite leqn0 => /nilP -> /=; apply: rotations_add_head. case: u => [_ | u0 u] //=; first exact: rotations_add_head. rewrite ltnS => Hsz t Htam0 Htam1. case: (leqP u0 (size u)) => Hu0; rewrite !(from_vct_accE t). - move/(Tamari_drop u0.+1): Htam0. move/(Tamari_drop u0.+1): Htam1. have dropl_cat d (s1 : seq nat) : d <= size s1 -> forall s2, drop d (s1 ++ s2) = drop d s1 ++ s2. rewrite leq_eqVlt => /orP[/eqP |] H s; rewrite drop_cat H //. by rewrite ltnn subnn drop0 drop_size. rewrite /= !(takel_cat _ Hu0) !(dropl_cat _ _ Hu0) => Htam0 Htam1. apply: IHn => //. rewrite size_drop leq_subLR. exact: leq_trans Hsz (leq_addl _ _). - have H0 : v0 < (u0 - size u).-1. rewrite -ltnS; apply: (leq_trans _ (leqSpred _)). rewrite -(ltn_add2r (size u)) subnK; last exact: ltnW. move/Tamari_consP: Htam1 => [_ _ /(_ _ Hu0)]. rewrite nth_cat ltnn subnn /=. rewrite -[(_ + v0).+1]addnS -addnA /=. exact: (leq_ltn_trans (leq_addl _ _)). move/Tamari_take: Htam0. move/Tamari_take: Htam1. rewrite !take_cat !drop_cat ltnNge (ltnW Hu0) /=. have:= Hu0; rewrite -subn_gt0 => /prednK <- /= => Htam0 Htam1. rewrite from_vct_cat_leftE [X in rotations X]from_vct_cat_leftE. apply catleft_rotations; apply rotations_right_sub. move: Htam0. have -> : nth 0 v v0 = nth 0 (take (u0 - size u).-1 v) v0 by rewrite nth_take. exact: IHn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype