proposition: Lemma num_of_listK x: list_of_num (num_of_list (rcons x true)) = rcons x true.
proof: Proof. by move:(pos_of_listK x); rewrite /num_of_list; case: rcons. 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)