proposition: Lemma wbase2_pad l k: wbase2 (l ++ nseq k ord0) = wbase2 l.
proof: Proof. suff: wbase2 (nseq k ord0) = 0 by move => h;rewrite wbase2_cat h muln0 addn0. by elim:k => // n /= ->. 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)