proposition: Lemma base2rev_oddI n: odd n -> base2rev (base2rev n) = n.
proof: Proof. move => on; have eq1 :=(oddE on). rewrite eq1 (base2rev_odd (odd_base2rev _)) - eq1 (base2rev_odd on). rewrite nat_of_binK eq1. case: {n on eq1} (n./2) => // n. rewrite -{2} (bin_of_natK (n.+1).*2.+1) bin_of_nato /= rev_cons num_of_listK. by rewrite - rev_cons revK (list_of_numK (Npos (pos_of_nat' n)~1)). 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)