proposition: Lemma Tamari_take v0 v : v0 :: v \is a TamariVector -> take v0 v \is a TamariVector.
proof: Proof. elim: v0 v => [| v0 IHv0] v; first by rewrite take0. case: v => [//= | v1 v]. move/Tamari_consP; rewrite /= ltnS => [] [Hsz Htam H]. apply/Tamari_consP; rewrite (size_takel Hsz). have:= H 0 (ltn0Sn _); rewrite ltnS addn0 => /= Hv1. split. - exact: Hv1. - apply: IHv0; move: Htam => /Tamari_consP[_ Hv H1]. apply/Tamari_consP; split => // i. by rewrite -ltnS => /H; rewrite /= ltnS addnS. - move/Tamari_consP: Htam {H} => [_ _ H] i Hi. by rewrite nth_take ?H // (leq_trans Hi Hv1). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype