proposition: Lemma odd_nonempty x: oddp (cardinal x) -> nonempty x.
proof: Proof. move => h; apply /nonemptyP => h1. move: h; rewrite h1 cardinal_set0; apply: odd_zero. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)