proposition: Theorem right_sizesK : cancel right_sizes from_vct.
proof: Proof. rewrite /from_vct => t. have [n] := ubnPleq (size_tree t); elim: n => [|n IHn] in t *. by rewrite leqn0 => /LeafP ->. rewrite -(left_branchK t). case/lastP: {t} (left_branch t) => //= [br r]. rewrite -cats1 -(from_leftK br) -(from_leftK [:: r]) -/(cat_left _ _) /=. rewrite right_sizes_cat_left /=. rewrite from_vct_accE -!size_right_sizes drop_size_cat // take_size_cat //. rewrite size_right_sizes size_cat_left /= addn0 add1n addnS ltnS => H. rewrite IHn /=; last exact: (leq_trans (leq_addl _ _) H). rewrite from_vct_cat_leftE. by rewrite IHn; last exact: (leq_trans (leq_addr _ _) H). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype