proposition: Lemma num_of_list_false x: num_of_list (rcons x false) = num_of_list (rcons x true).
proof: Proof. case: x => // a l; rewrite !rcons_cons /num_of_list; congr Npos. rewrite -!rcons_cons; elim: (a::l) => // {l} a l /= ->. move: (rev_cons true (rev l)) (rev_cons false (rev l)); rewrite revK. by rewrite split_rev (split_rev false) => <- <-. 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)