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