proposition: Lemma clog1 : clog2 \1c = \1c.
proof: Proof. rewrite - {2} succ_zero;apply: (clog_pr NS1 NS0). rewrite cpowx0; fprops. rewrite succ_zero (cpowx1 CS2); apply: clt_12. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)