proposition: Lemma Tamari_add_min u v0 v w0 w : u ++ w0 :: w \is a TamariVector -> u ++ v0 :: v <=V u ++ w0 :: w -> v0 < w0 -> nth 0 v v0 + v0 < w0.
proof: Proof. move/Tamari_catr/Tamari_consP => [_ _ Hv] Hleq /Hv/(leq_ltn_trans _); apply. rewrite leq_add2r. move/vctleqP : Hleq => [_ /(_ ((size u) + v0.+1))]. rewrite !nth_cat /=. by rewrite [_ + _ < _]ltnNge leq_addr /= addKn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype