proposition: Lemma base2rev_oddII p (n := (base2rev p)): base2rev (base2rev n) = n.
proof: Proof. by rewrite /n {n}; case: p => // n; apply: base2rev_oddI; exact: odd_base2rev. 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)