proposition: Lemma clog_pr n m: natp n -> natp m -> \2c ^c m <=c n -> n <c \2c ^c (csucc m) -> clog2 n = csucc m.
proof: Proof. move => nN mN eq1 eq2. case: (equal_or_not n \0c) => nz. by move: eq1; rewrite nz => /cle0 =>/ (cpow_nz card2_nz). move:(clog_nz nN nz) => [lN lz eq3 eq4]. move:(cle_ltT eq1 eq4) => /(cpow2_MeqltP mN lN) /(cleSltP mN); apply:cleA. move:(cpred_pr lN lz) => [sc sd]. move:(cle_ltT eq3 eq2) => /(cpow2_MeqltP sc (NS_succ mN)) /(cleSltP sc); ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)