proposition: Lemma num_of_list_sizeK x: size (list_of_num (num_of_list x)) = size x.
proof: Proof. rewrite -(revK x);case: {x} (rev x) => // b l. by case: b; rewrite rev_cons ?num_of_list_false num_of_listK // !size_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)