proposition: Lemma nat_of_list_rT l: nat_of_list (rcons l true) = nat_of_bin (num_of_list (rcons l true)).
proof: Proof. elim: l => // a l /= -> /=; rewrite /num_of_list headI - headI. by case:a; case: l => // a l; rewrite /= natTrecE. 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)