proposition: Lemma nat_of_list_ext k l: nat_of_list (l ++ nseq k false) = nat_of_list l.
proof: Proof. elim:k l => [l | n H l /=]; first by rewrite cats0. by rewrite - cat_rcons H - nat_of_list_rF. 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)