proposition: Theorem from_vctK : {in TamariVector, cancel from_vct right_sizes}.
proof: Proof. rewrite /from_vct => s. have [n] := ubnPleq (size s); elim: n => [|n IHn] in s *. by rewrite leqn0 => /nilP ->. case: s => [| s0 s] //=. rewrite ltnS -{1}(cat_take_drop s0 s) size_cat => Hsz Hcons. have:= Hcons => /Tamari_consP[Hs0 Hs Hall]. rewrite from_vct_accE from_vct_cat_leftE right_sizes_cat_left. rewrite IHn /=; first last. - exact: Tamari_drop. - exact: (leq_trans (leq_addl _ _) Hsz). rewrite {}IHn /=; first last. - exact: Tamari_take. - exact: (leq_trans (leq_addr _ _) Hsz). by rewrite cat_take_drop size_from_vct_acc size_takel. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype