proposition: Lemma prime_oddPn p : prime p -> reflect (p = 2) (~~ odd p).
proof: Proof. by move=> p_pr; apply: (iffP idP) => [|-> //]; case/even_prime: p_pr => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)