proposition: Lemma Tamari_cat v1 v2 : v1 \is a TamariVector -> v2 \is a TamariVector -> v1 ++ v2 \is a TamariVector.
proof: Proof. elim: v1 => [| v0 v1 IHv1] //= /Tamari_consP[Hv0 Hv1 Hall] Hv2. apply/Tamari_consP; split. - rewrite size_cat; apply: (leq_trans Hv0); apply leq_addr. - exact: IHv1. - by move=> i Hi; rewrite nth_cat (leq_trans Hi Hv0) Hall. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype