proposition: Lemma card_wbase2_odd n: card_wbase2 n.*2.+1 = card_wbase2 n.
proof: Proof. have sd:= (log2_Sdouble n). rewrite (card_wbase2_invariant (leqnn (log2 n))). rewrite (card_wbase2_invariant (leqnn (log2 n.*2.+1))) sd. rewrite /card_wbase2'. set T1 := (log2 n).-tuple 'I_3. set T2 := (log2 n).+1.-tuple 'I_3. have sz: forall z:T1, size (in_tuple (ord1_3::z)) = (log2 n).+1. by move => z;rewrite !size_tuple. set g:(T1 -> T2) := (fun z => (tcast (sz z) (in_tuple (ord1_3::z)))). have ig: injective g. move => z1 z2 ww; apply: val_inj. have: (tval (g z1) = tval (g z2)) by rewrite ww. by rewrite /g !tcast_val /=; case. symmetry. rewrite -(card_imset _ ig). apply: eq_card => t; rewrite inE; apply/imsetP/idP. by move => [x]; rewrite inE => xp ->; rewrite /g tcast_val /= (eqP xp). move=> /eqP /wbase2_odd1; move: (erefl (tval t)). case: {-1} (tval t) => [ tv [] // | a l /= tv [av lv]]. have sl:(size (in_tuple l)) = log2 n. by apply/eqP; rewrite -eqSS - (size_tuple t) tv. exists (tcast sl (in_tuple l)); first by rewrite inE tcast_val /= lv. by apply: val_inj; rewrite /g /= tv av! tcast_val //. 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)