proposition: Lemma base2r_oddp n: natp n -> n <> \0c -> oddp (base_two_reverse n).
proof: Proof. move: n; apply: fusc_induction. + by case. + rewrite base2r_one => _; apply: odd_one. + move => k kN H ck. by rewrite (base2r_even kN); apply: H => h; case:ck; rewrite h cdouble0. + move =>k kN Ha _ ck. rewrite (base2r_odd kN). case: (equal_or_not k \0c) => knz. rewrite knz clog0 base2r_zero cpowx0 (csum0r CS1); apply: odd_one. apply: (csum_of_even_odd (power2_log_even kN knz) (Ha knz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)