proposition: Lemma clog_nz n (m := clog2 n): natp n -> n <> \0c -> [/\ natp m, m <> \0c, \2c ^c (cpred m) <=c n & n <c \2c ^c m].
proof: Proof. move => nN nz; move: (CS_nat nN) => cn. rewrite /m /clog2; set p := (fun z => n <c \2c ^c z); clear m. have pn: p n by apply: (cantor cn). move: (least_ordinal4 (OS_cardinal cn) pn); set m:= (least_ordinal p n). move => [sa sb sc]. move:(sc _ (OS_cardinal cn) pn) => le1. have mN: natp m. apply /(oltP OS_omega); move/(oltP OS_omega):nN => h; exact:ole_ltT le1 h. case: (equal_or_not m \0c) => mz. by case:nz; move: sb; rewrite /p mz cpowx0 => /clt1. move: (cpred_pr mN mz) => [ha hb]. split => //; case: (NleT_el (NS_pow NS2 ha) nN) => // lt2. move: (cpred_lt mN mz) => /oclt lt3. case:(oltNge lt3 (sc _ (proj31_1 lt3) lt2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)