proposition: Lemma from_vct_accE lft v0 vct : from_vct_acc lft (v0 :: vct) = from_vct_acc (BinNode lft (from_vct_acc BinLeaf (take v0 vct))) (drop v0 vct).
proof: Proof. rewrite -[in RHS](from_vct_fuelE (fuel := size (v0 :: vct))); first last. by rewrite /= ltnS size_drop leq_subr. rewrite {2}/from_vct_acc. rewrite -[_ _.+1 _ _](from_vct_fuelE (fuel := size (v0 :: vct))); first by []. by rewrite /= size_take -/(minn _ _) ltnS geq_minr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype