proposition: Lemma wbase2_correct n: wbase2 [seq bool_to_I3 i | i<- (list_of_num (bin_of_nat n))] = n.
proof: Proof. case: n => // n; rewrite - {2}(pos_of_natK n) /= /pos_of_nat'. by elim: (pos_of_nat n n) => //= p ->; rewrite natTrecE //. 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)