proposition: Lemma NS_reverse n: natp n -> natp (base_two_reverse n).
proof: Proof. move: n; apply: fusc_induction. + rewrite base2r_zero; fprops. + rewrite base2r_one; fprops. + by move => k kn; rewrite base2r_even. + move => k kn sa _; rewrite ( base2r_odd kn); apply:NS_sum sa. apply:(NS_pow NS2 (NS_log kn)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)