proposition: Lemma rotations_add_bounded u v0 v w0 w : u ++ v0 :: v \is a TamariVector -> u ++ w0 :: w \is a TamariVector -> u ++ v0 :: v <=V u ++ w0 :: w -> v0 < w0 -> from_vct (u ++ (nth 0 v v0 + v0).+1 :: v) \in rotations (from_vct (u ++ v0 :: v)).
proof: Proof. move=> Hv Hw Hleq H0. apply: rotations_add => //. exact: (Tamari_add_bounded Hv Hw Hleq H0). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype