proposition: Lemma log2_pr1 n (k := \2c ^c (cpred (clog2 n))) : natp n -> n <> \0c -> n = k +c (n %%c k).
proof: Proof. move => nN nz. move:(clog_nz nN nz) => [sa sb]; rewrite /k. move: (cpred_pr sa sb) => []; set m := cpred (clog2 n). move => mN mv sc sd. move: (cdivision nN (NS_pow NS2 mN) (@cpow2_nz m)) => [qN rN Ha]. move/(cdivision_prop_alt nN (NS_pow NS2 mN) qN rN (@cpow2_nz m)):(Ha). move: Ha => [nv rs] [hu hv _]. case: (equal_or_not (n %/c \2c ^c m) \0c) => qnz. by move: (cle_ltT sc hv); rewrite qnz succ_zero (cprod1r (proj31 sc)); case. move:(cle_ltT hu sd); rewrite mv - (cdouble_pow2 mN) cprodC. move/(cprod_lt2r (NS_pow NS2 mN) qN NS2) /clt2; case => // eq1. move: nv; rewrite eq1 cprod1r//; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)