proposition: Lemma Tamari_add_bounded u v0 v w0 w : u ++ v0 :: v \is a TamariVector -> u ++ w0 :: w \is a TamariVector -> u ++ v0 :: v <=V u ++ w0 :: w -> v0 < w0 -> u ++ (nth 0 v v0 + v0).+1 :: v \is a TamariVector.
proof: Proof. elim: u => [| u0 u IHu] Hv Hw /= Hleq H0. apply Tamari_add_head; first by []. move: Hleq => /vctleqP[/=/eq_add_S -> _]; apply (leq_trans H0). by have:= Hw => /Tamari_consP[]. apply/Tamari_consP; split. - by move/Tamari_consP: Hv => []; rewrite !size_cat /=. - apply: IHu => //. + by move/Tamari_consP: Hv => []. + by move/Tamari_consP: Hw => []. + move: Hleq; rewrite /vctleq /= => /and3P[]. by rewrite eqSS => -> _ ->. - move=> i Hi {IHu}; rewrite nth_cat. case: (ltngtP i (size u)) => Hiu. + move/Tamari_consP: Hv => [_ _ /(_ i Hi)]. by rewrite nth_cat Hiu. + have/Tamari_consP := Hv => [] [_ _ /(_ i Hi)]. rewrite nth_cat [i < size u]ltnNge (ltnW Hiu) /=. move: Hiu; rewrite -subn_gt0. by case: (i - size u). + subst i; rewrite subnn /=. have/Tamari_consP := Hw => [] [_ _ /(_ _ Hi)]. rewrite nth_cat ltnn subnn /= => /(leq_ltn_trans _); apply. rewrite leq_add2r. exact: Tamari_add_min Hw Hleq H0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype