proposition: Lemma oddp_mod2 n: natp n -> (oddp n <-> n = \1c %c[mod \2c]).
proof: Proof. move => nN; rewrite crem_12; apply: (iff_trans (oddp_alt n)). by split; [case|]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)