proposition: Lemma cle_halfn_n n: natp n -> chalf n <=c n.
proof: Proof. move => nN. have H:=(cle_n_doublen (NS_half nN)). case:(cdouble_halfV nN); move => {2} -> //. apply: (cleT H (cleS (NS_double (NS_half nN)))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)