proposition: Lemma base2r_oddK_bis n (r := base_two_reverse) : natp n -> r (r (r n)) = r n.
proof: Proof. move => nN. case: (equal_or_not n \0c) => nz; first by rewrite nz /r !base2r_zero. by apply:base2r_oddK; apply: base2r_oddp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)