proposition: Lemma card_wbase2_even n: card_wbase2 n.*2.+2 = card_wbase2 n + card_wbase2 n.+1.
proof: Proof. move: (log2_double n); rewrite doubleS => ds. set k := (log2 n.+1). rewrite (card_wbase2_invariant (leqnn (log2 n.*2.+2))) ds -/k. rewrite /card_wbase2'. set T1 := k.-tuple 'I_3. set T2 := k.+1.-tuple 'I_3. set A := [set t:T2 | wbase2 t == n.*2.+2]. set B := [set t:T2 | (wbase2 t == n.*2.+2) && (head ord0 t == ord0)]. set C := [set t:T2 | (wbase2 t == n.*2.+2) && (head ord0 t == ord2_3)]. have dab: A :&: B = B. by apply/setIidPr/subsetP => x; rewrite /A/B !inE => /andP[]. have dac: A:\: B = C. apply /setP => x; rewrite /A/B/C !inE; case ww:(wbase2 x == n.*2.+2) => //=. rewrite andbT; move: (wbase2_double_nz (eqP ww))=> [_]. case ta: (head ord0 x == ord0); first by rewrite (eqP ta) //. by move/andP => [/eqP ->]. rewrite -(cardsID B A) dab dac addnC; congr addn; symmetry. have l2b:log2 n <= k by apply: leqn_log. rewrite /C (card_wbase2_invariant l2b) /card_wbase2'. have sz: forall z:T1, size (in_tuple (ord2_3::z)) = k.+1. by move => z;rewrite !size_tuple. set g:(T1 -> T2) := (fun z => (tcast (sz z) (in_tuple (ord2_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. rewrite -(card_imset _ ig). apply: eq_card => t; rewrite inE; apply/imsetP/idP. move => [x]; rewrite inE => xp ->. by rewrite /g tcast_val /= (eqP xp) add2n !eqxx //. move=> /andP[/eqP /wbase2_double_nz [tv]]; case:eqP; first by move => ->. move => _ /andP [sa sb] _. move /eqP: (f_equal size tv); rewrite size_tuple /= eqSS => /eqP sl1. have sl:(size (in_tuple (behead t))) = k by rewrite /= -sl1. exists (tcast sl (in_tuple (behead t))); first by rewrite inE tcast_val. by apply: val_inj; rewrite /g /= {1} tv (eqP sa) !tcast_val. rewrite /C (card_wbase2_invariant (leqnn k)) /card_wbase2'. have sz: forall z:T1, size (in_tuple (ord0::z)) = k.+1. by move => z;rewrite !size_tuple. set g:(T1 -> T2) := (fun z => (tcast (sz z) (in_tuple (ord0::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. rewrite -(card_imset _ ig). apply: eq_card => t; rewrite inE; apply/imsetP/idP. move => [x]; rewrite inE => xp ->. by rewrite /g tcast_val /= (eqP xp) doubleS !eqxx. move=> /andP[/eqP /wbase2_double_nz [tv ta tb]]. move: ta; rewrite tb (eqP tb) /= addbF => tc. move /eqP: (f_equal size tv); rewrite size_tuple /= eqSS => /eqP sl1. have sl:(size (in_tuple (behead t))) = k by rewrite /= -sl1. exists (tcast sl (in_tuple (behead t))); first by rewrite inE tcast_val. by apply: val_inj; rewrite /g /= {1} tv (eqP tb) !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)