proposition: Lemma nat_of_list_rF l : nat_of_list l = nat_of_list (rcons l false).
proof: Proof. by elim: l => // a s /= ->. 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)