proposition: Lemma Tamari_add_head v0 v : v0 :: v \is a TamariVector -> v0 < size v -> (nth 0 v v0 + v0).+1 :: v \is a TamariVector.
proof: Proof. move => /Tamari_consP[_ Hv Htam0] Hv0. have /TamariP[Hc Htamv] := Hv. apply/Tamari_consP; split => //; first exact: Hc. move=> i; rewrite !ltnS => H. case: (ltngtP i v0) => [ltnv0i | ltniv0 | -> //]. + exact: leq_trans (ltnW (Htam0 i ltnv0i)) (leq_addl _ _). + by apply: Htamv; rewrite ltniv0 H. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype