proposition: Lemma dvdp_gcd p m n : p %| gcdp m n = (p %| m) && (p %| n).
proof: Proof. apply/idP/andP=> [dv_pmn | []]. by rewrite ?(dvdp_trans dv_pmn) ?dvdp_gcdl ?dvdp_gcdr. have [r] := ubnP (minn (size n) (size m)); elim: r => // r IHr in m n *. have [-> | nz_m] := eqVneq m 0; first by rewrite gcd0p. have [-> | nz_n] := eqVneq n 0; first by rewrite gcdp0. rewrite gcdpE ltnS; case: leqP => [le_nm | lt_mn] le_r dv_m dv_n. apply: IHr => //; last by rewrite -(dvdp_mod _ dv_n). by rewrite gtn_min orbC (leq_trans _ le_r) ?ltn_modp. apply: IHr => //; last by rewrite -(dvdp_mod _ dv_m). by rewrite gtn_min orbC (leq_trans _ le_r) ?ltn_modp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)