proposition: Lemma primeP p : reflect (p > 1 /\ forall d, d %| p -> xpred2 1 p d) (prime p).
proof: Proof. rewrite -[prime p]negbK; have [npr_p | pr_p] := primePn p. right=> [[lt1p pr_p]]; case: npr_p => [|[d n1pd]]. by rewrite ltnNge lt1p. by move/pr_p=> /orP[] /eqP def_d; rewrite def_d ltnn ?andbF in n1pd. have [lep1 | lt1p] := leqP; first by case: pr_p; left. left; split=> // d dv_d_p; apply/norP=> [[nd1 ndp]]; case: pr_p; right. exists d; rewrite // andbC 2!ltn_neqAle ndp eq_sym nd1. by have lt0p := ltnW lt1p; rewrite dvdn_leq // (dvdn_gt0 lt0p). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)