proposition: Lemma wbase2_exists n k: log2 n <= k -> exists l:(k.-tuple 'I_3), wbase2 l = n.
proof: Proof. move => lk. set l := [seq bool_to_I3 i | i<- (list_of_num (bin_of_nat n))] ++ (nseq (k - log2 n) ord0). have sl: size l = k by rewrite /l size_cat size_map size_nseq -/(log2 n) subnKC. exists (tcast sl (in_tuple l)). by rewrite tcast_val in_tupleE /l wbase2_pad wbase2_correct. 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)