proposition: Lemma log2_pr2 n : natp n -> clog2 n = cardinal (domain (the_expansion \2c n)).
proof: Proof. move => nN. case: (equal_or_not n \0c) => nz. by rewrite nz (the_expansion_zero NS2 clt_12) clog0 domain_set0 cardinal_set0. move:(base2_expansion_prop nN nz). set c := cardinal _; move => [[sa sb] cz sd]. move: (sa) => [_ cN _ _]. move: (cpred_pr cN cz) => [se sf]. move: (expansion_prop9 sa); rewrite sb sf;apply: (clog_pr nN se). rewrite sf in sa. have ca: cardinalp (\2c ^c cpred c) by fprops. rewrite - sb (expansion_prop7 sa (CS_nat se)) sd (cprod1l ca). by apply: csum_Mle0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)