proposition: Lemma power2_log_even n: natp n -> n <> \0c -> evenp (\2c ^c (clog2 n)).
proof: Proof. move => nN nz; move:(clog_nz nN nz) => [sa sb sc sd]. move:(cpred_pr sa sb) => [ha hb]; rewrite hb - (cdouble_pow2 ha). by apply: (even_double (NS_pow NS2 ha)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)