proposition: Lemma succ_of_odd n: oddp n -> evenp (csucc n).
proof: Proof. move /(oddp_alt) => [nN sa]. by split;fprops; rewrite (crem_succ nN NS2 clt_12) sa succ_one crem_22. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)