proposition: Lemma Tamari_catr u v : u ++ v \is a TamariVector -> v \is a TamariVector.
proof: Proof. by move=> /(Tamari_drop (size u)); rewrite drop_cat ltnn subnn drop0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype