proposition: Lemma succ_of_oddP n: natp n -> (oddp n <-> evenp (csucc n)).
proof: Proof. move => nN; split; first by apply:succ_of_odd. by move => h;case: (p_or_not_p (evenp n)) => // /succ_of_even []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)