proposition: Lemma from_vct_cat_leftE lft vct : from_vct_acc lft vct = cat_left (from_vct_acc BinLeaf vct) lft.
proof: Proof. have [n/ltnW] := ubnP (size vct); elim: n => [|n IHn] in vct lft * => /ltnSE. by rewrite leqn0 /from_vct_acc => /nilP ->; rewrite /= cat_left0t. case: vct => [_ | v0 v] /=. by rewrite /from_vct_acc /= cat_left0t. rewrite ltnS -{1}(cat_take_drop v0 v) size_cat !from_vct_accE /=. move: (take v0 v) (drop v0 v) => {v0 v} u v Huv. rewrite IHn; last exact: (leq_trans (leq_addl _ _) Huv). rewrite [in RHS]IHn; last exact: (leq_trans (leq_addl _ _) Huv). by rewrite cat_leftA cat_left_Node. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype