proposition: Lemma wbase2_zero l : wbase2 l = 0 -> l = nseq (size l) ord0.
proof: Proof. move => h; apply /all_pred1P. elim:l h=> // a l Hr /= /eqP; rewrite addn_eq0 double_eq0=> /andP[/eqP ha /eqP]. by move/Hr => ->; rewrite andbT; apply/eqP; apply:val_inj. 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)