proposition: Lemma vctmin_Tamari v1 v2 : size v1 = size v2 -> v1 \is a TamariVector -> v2 \is a TamariVector -> vctmin v1 v2 \is a TamariVector.
proof: Proof. move=> Hsz /TamariP[Hleq1 H1] /TamariP[Hleq2 H2]. apply/TamariP; rewrite size_vctmin Hsz minnn; split. - move=> i Hi {Hleq1 H1 H2}; rewrite nth_vctmin addn_minl. exact: leq_ltn_trans (geq_minr _ _) (Hleq2 _ Hi). - move=> i j {Hleq1 Hleq2}; rewrite !nth_vctmin !addn_minl. rewrite leq_min=> /andP[Hij /andP[Hj1 Hj2]]. by rewrite leq_min !geq_min H1 /= ?H2 ?orbT // Hij. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype