proposition: Lemma clog_double n: natp n -> n <> \0c -> clog2 (cdouble n) = csucc (clog2 n).
proof: Proof. move => nN nz. move:(clog_nz nN nz) => [sa sb sc sd]; apply:(clog_pr (NS_double nN) sa). move: (cpred_pr sa sb) => [ha ->]; rewrite - (cdouble_pow2 ha). by apply/(double_monotone (NS_pow NS2 ha) nN). by rewrite - (cdouble_pow2 sa); apply /(double_monotone2 nN (NS_pow NS2 sa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)