proposition: Lemma dvdn_prime2 p q : prime p -> prime q -> (p %| q) = (p == q).
proof: Proof. move=> pr_p pr_q; apply: negb_inj. by rewrite eqn_dvd negb_and -!prime_coprime // coprime_sym orbb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)