proposition: Lemma even_prime p : prime p -> p = 2 \/ odd p.
proof: Proof. move=> pr_p; case odd_p: (odd p); [by right | left]. have: 2 %| p by rewrite dvdn2 odd_p. by case/primeP: pr_p => _ dv_p /dv_p/(2 =P p). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)