proposition: Lemma primePns n : reflect (n < 2 \/ exists p, [/\ prime p, p ^ 2 <= n & p %| n]) (~~ prime n).
proof: Proof. apply: (iffP idP) => [npr_p|]; last first. case=> [|[p [pr_p le_p2_n dv_p_n]]]; first by case: n => [|[]]. apply/negP=> pr_n; move: dv_p_n le_p2_n; rewrite dvdn_prime2 //; move/eqP->. by rewrite leqNgt -[ltnLHS]muln1 ltn_pmul2l ?prime_gt1 ?prime_gt0. have [lt1p|] := leqP; [right | by left]. exists (pdiv n); rewrite pdiv_dvd pdiv_prime //; split=> //. by case: leqP npr_p => // /ltn_pdiv2_prime -> //; exact: ltnW. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)