proposition: Lemma nat_of_list_rT' l: ends_with_a l true -> nat_of_list l = nat_of_bin (num_of_list l).
proof: Proof. by move/ends_with_aP => [w ->]; apply:nat_of_list_rT. 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)