proposition: Lemma wbase2_split l n: log2 n <= size l -> wbase2 l = n -> l = take (log2 n) l ++ nseq ((size l) - log2 n) ord0.
proof: Proof. move => sa sb. move: (size_takel sa)(cat_take_drop (log2 n) l) => sc sd. move: sb; rewrite -{1 2} sd wbase2_cat sc => ea. have: n < 2 ^ log2 n by clear; case: n => // n; move/andP:(log2_bnd n) =>[]. rewrite - {1} ea; case: (posnP (wbase2 (drop (log2 n) l))) => res. by move => _; rewrite (wbase2_zero res) size_drop. move => h. by move: (leq_trans h (leq_pmulr ( 2 ^ log2 n) res));rewrite ltnNge leq_addl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)