proposition: Lemma prime_coprime p m : prime p -> coprime p m = ~~ (p %| m).
proof: Proof. case/primeP=> p_gt1 p_pr; apply/eqP/negP=> [d1 | ndv_pm]. case/dvdnP=> k def_m; rewrite -(addn0 m) def_m gcdnMDl gcdn0 in d1. by rewrite d1 in p_gt1. by apply: gcdn_def => // d /p_pr /orP[] /eqP->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)