proposition: Lemma ltn_pdiv2_prime n : 0 < n -> n < pdiv n ^ 2 -> prime n.
proof: Proof. case def_n: n => [|[|n']] // _; rewrite -def_n => lt_n_p2. suffices ->: n = pdiv n by rewrite pdiv_prime ?def_n. apply/eqP; rewrite eqn_leq leqNgt andbC pdiv_leq; last by rewrite def_n. apply/contraL: lt_n_p2 => lt_pm_m; case/dvdnP: (pdiv_dvd n) => q def_q. rewrite -leqNgt [leqRHS]def_q leq_pmul2r // pdiv_min_dvd //. by rewrite -[pdiv n]mul1n [ltnRHS]def_q ltn_pmul2r in lt_pm_m. by rewrite def_q dvdn_mulr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)