proposition: Lemma card_wbase2_invariant k n : log2 n <= k -> card_wbase2 n = card_wbase2' k n.
proof: Proof. move => lk;move:(tuple_pad_injective (H:=lk)) => ti. rewrite /card_wbase2 /card_wbase2' -(card_imset _ ti). apply: eq_card => t; rewrite inE; apply/imsetP/idP. by move => [x]; rewrite inE => xp ->; rewrite wbase2_tuple_pad. move => wtn. have sizet: log2 n <= size t by rewrite size_tuple. move:(wbase2_split sizet (eqP wtn)) => tv. set x := take (log2 n) t . have sx: size x = log2 n by rewrite /= size_takel. set x' := tcast sx (in_tuple x). have tv': t = tuple_pad x' lk. by apply:val_inj; rewrite /= tuple_pad_val tv size_tuple !tcast_val. by exists x' => //; rewrite inE // - {2}(eqP wtn) tv' wbase2_tuple_pad. 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)