proposition: Lemma oddp_alt n: (oddp n <-> natp n /\ n %%c \2c = \1c).
proof: Proof. split => [] [nN on]; split => //. move: (cdivision nN NS2 card2_nz) => [ _ mN [_ /clt2]]; case => // h. by case:on. case=> _; rewrite on; exact:card1_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)