proposition: Lemma log2_pow n: natp n -> clog2 (\2c ^c n) = (csucc n).
proof: Proof. move => nN; move: (NS_pow NS2 nN) => pN. apply:(clog_pr pN nN (proj33 (NleR pN))). apply/(cpow2_MeqltP nN (NS_succ nN)); apply/(cltS nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)