proposition: Lemma from_vct_fuelE fuel lft vct : size vct < fuel -> from_vct_rec fuel lft vct = from_vct_acc lft vct.
proof: Proof. rewrite /from_vct_acc. have [fuel1] := ubnPleq (size vct).+1. elim: fuel => [| fuel IHfuel] in vct fuel1 lft *. by move=> /leq_trans /[apply]. case: fuel1 => // fuel1; rewrite !ltnS. case: vct => // v0 vct /= Hsz Hfuel1. rewrite !(IHfuel _ fuel1) //. - by rewrite size_take; exact: (leq_ltn_trans (geq_minr _ _) Hsz). - by rewrite size_drop; exact: (leq_ltn_trans (leq_subr _ _) Hsz). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype