proposition: Lemma clog0 : clog2 \0c = \0c.
proof: Proof. rewrite /clog2. set p := (fun z => \0c <c \2c ^c z). have h: p \0c by rewrite /p cpowx0; apply: clt_01. by move:(least_ordinal1 OS0 h) => [_ _ hc]; move: (hc _ OS0 h) => /sub_set0 ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)