proposition: Lemma primePn n : reflect (n < 2 \/ exists2 d, 1 < d < n & d %| n) (~~ prime n).
proof: Proof. rewrite /prime; case: n => [|[|p2]]; try by do 2!left. case: (@prime_decomp_correct p2.+2) => //; rewrite unlock. case: prime_decomp => [|[q [|[|e]]] pd] //=; last first; last by rewrite andbF. rewrite {1}/pfactor 2!expnS -!mulnA /=. case: (_ ^ _ * _) => [|u -> _ /andP[lt1q _]]; first by rewrite !muln0. left; right; exists q; last by rewrite dvdn_mulr. have lt0q := ltnW lt1q; rewrite lt1q -[ltnLHS]muln1 ltn_pmul2l //. by rewrite -[2]muln1 leq_mul. rewrite {1}/pfactor expn1; case: pd => [|[r e] pd] /=; last first. case: e => [|e] /=; first by rewrite !andbF. rewrite {1}/pfactor expnS -mulnA. case: (_ ^ _ * _) => [|u -> _ /and3P[lt1q ltqr _]]; first by rewrite !muln0. left; right; exists q; last by rewrite dvdn_mulr. by rewrite lt1q -[ltnLHS]mul1n ltn_mul // -[q.+1]muln1 leq_mul. rewrite muln1 !andbT => def_q pr_q lt1q; right=> [[]] // [d]. by rewrite def_q -mem_index_iota => in_d_2q dv_d_q; case/hasP: pr_q; exists d. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)