proposition: Lemma succ_of_evenP n: natp n -> (evenp n <-> oddp (csucc n)).
proof: Proof. move => nN; split; first by apply:succ_of_even. move => h;ex_middle h';case: (proj2 h);exact:(succ_of_odd (conj nN h')). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)