proposition: Lemma cle_halfSn_n n: natp n -> chalf (csucc n) <=c n.
proof: Proof. move => nN. case: (equal_or_not n \0c) => nz. rewrite nz succ_zero half1; fprops. move:(cpred_pr nN nz) => [sa sb]; rewrite sb (half_succ sa). by move/(cleSSP (CS_nat (NS_half sa)) (CS_nat sa)): (cle_halfn_n sa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)