proposition: Lemma dvdp_gcdlr p q : (gcdp p q %| p) && (gcdp p q %| q).
proof: Proof. have [r] := ubnP (minn (size q) (size p)); elim: r => // r IHr in p q *. have [-> | nz_p] := eqVneq p 0; first by rewrite gcd0p dvdpp andbT. have [-> | nz_q] := eqVneq q 0; first by rewrite gcdp0 dvdpp /=. rewrite ltnS gcdpE; case: leqP => [le_pq | lt_pq] le_qr. suffices /IHr/andP[E1 E2]: minn (size q) (size (p %% q)) < r. by rewrite E2 andbT (dvdp_mod _ E2). by rewrite gtn_min orbC (leq_trans _ le_qr) ?ltn_modp. suffices /IHr/andP[E1 E2]: minn (size p) (size (q %% p)) < r. by rewrite E2 (dvdp_mod _ E2). by rewrite gtn_min orbC (leq_trans _ le_qr) ?ltn_modp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)