proposition: Lemma dvdn_gcd p m n : p %| gcdn m n = (p %| m) && (p %| n).
proof: Proof. apply/idP/andP=> [dv_pmn | [dv_pm dv_pn]]. by rewrite !(dvdn_trans dv_pmn) ?dvdn_gcdl ?dvdn_gcdr. have [->|n_gt0] := posnP n; first by rewrite gcdn0. case: (Bezoutr m n_gt0) => // km _ /(dvdn_trans dv_pn). by rewrite dvdn_addl // dvdn_mull. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)