proposition: Lemma size_from_vct_acc s : size_tree (from_vct_acc BinLeaf s) = size s.
proof: Proof. have [n/ltnW] := ubnP (size s); elim: n => [|n IHn] in s * => /ltnSE. by rewrite leqn0 => /nilP ->. case: s => [| s0 s] //=. rewrite ltnS -{1}(cat_take_drop s0 s) size_cat => Hsz. rewrite from_vct_accE from_vct_cat_leftE. rewrite size_cat_left /= addn0 add1n addnS. rewrite IHn; last exact: (leq_trans (leq_addl _ _) Hsz). rewrite IHn; last exact: (leq_trans (leq_addr _ _) Hsz). by rewrite addnC -size_cat cat_take_drop. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype