proposition: Lemma wbase2_cat l1 l2: wbase2 (l1 ++ l2) = wbase2 l1 + (2^(size l1)) * (wbase2 l2).
proof: Proof. elim: l2 l1; first by move => l1; by rewrite muln0 addn0 cats0. move => a l2 H l1;rewrite - cat_rcons H size_rcons /= mulnDr addnA. by rewrite -doubleMr doubleMl -expn2S wbase2_recr. 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)