proposition: Lemma succ_of_even n: evenp n -> oddp (csucc n).
proof: Proof. move => [nN h]; split; [fprops | case => _]. rewrite (crem_succ nN NS2 clt_12) h succ_zero crem_12; apply:card1_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)