proposition: Lemma clog_succ_double n: natp n -> clog2 (csucc (cdouble n)) = csucc (clog2 n).
proof: Proof. move => nN. case: (equal_or_not n \0c) => nz. rewrite nz /cdouble clog0 cprod0r {1} succ_zero; apply:(clog_pr NS1 NS0). rewrite cpowx0; fprops. rewrite succ_zero;apply: (cantor CS1). move:(clog_nz nN nz) => [sa sb sc sd]. apply:(clog_pr (NS_succ (NS_double nN)) sa). move: (cpred_pr sa sb) => [ha ->]; rewrite - (cdouble_pow2 ha). apply: cleT (cleS (NS_double nN)). by apply/(double_monotone (NS_pow NS2 ha) nN). by rewrite - (cdouble_pow2 sa); apply /(double_monotone3 nN (NS_pow NS2 sa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)