proposition: Lemma prime_nt_dvdP d p : prime p -> d != 1 -> reflect (d = p) (d %| p).
proof: Proof. case/primeP=> _ min_p d_neq1; apply: (iffP idP) => [/min_p|-> //]. by rewrite (negPf d_neq1) /= => /eqP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)