proposition: Lemma Tamari_drop n v : v \is a TamariVector -> drop n v \is a TamariVector.
proof: Proof. rewrite !unfold_in; elim: n v => [//= | n IHn] v; first by rewrite drop0. by case: v => [| v0 v] //= /and3P[_ /IHn ->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype