proposition: Lemma card_wbase2_val n: card_wbase2 n = fusc n.+1.
proof: Proof. have wz:card_wbase2 0 = fusc 1. rewrite /card_wbase2 /card_wbase2' /fusc /=. set T := (log2 0).-tuple 'I_3. suff: [set t:T | wbase2 t == 0] = [set t:T | predT t]. by move => ->; rewrite cardsE /= card_tuple expn0. by apply /setP => t; rewrite ! inE; move: (size_tuple t); case: (tval t). elim: n {-2} n (leqnn n) => [ []| n Hrec [|m]] //. rewrite ltnS -(odd_double_half m);case:(odd _) => h. have la:=(leq_ltn_trans (double_le1 m./2) h). by rewrite add1n card_wbase2_even -doubleS fusc_odd (Hrec _ (ltnW la)) Hrec. rewrite add0n card_wbase2_odd - doubleS fusc_even Hrec //. exact (leq_trans (double_le1 m./2) h). 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)