proposition: Lemma dvdp_gdcor p q : q != 0 -> p %| (gdcop q p) * (q ^+ size p).
proof: Proof. rewrite /gdcop => nz_q; have [n hsp] := ubnPleq (size p). elim: n => [|n IHn] /= in p hsp *; first by rewrite (negPf nz_q) mul0r dvdp0. have [_ | ncop_pq] := ifPn; first by rewrite dvdp_mulr. have g_gt1: 1 < size (gcdp p q). rewrite ltn_neqAle eq_sym ncop_pq size_poly_gt0 gcdp_eq0. by rewrite negb_and nz_q orbT. have [-> | nz_p] := eqVneq p 0. by rewrite div0p exprSr mulrA dvdp_mulr // IHn // size_poly0. have le_d_p: size (p %/ gcdp p q) < size p. rewrite size_divp -?size_poly_eq0 -(subnKC g_gt1) // add2n /=. by rewrite polySpred // ltnS subSS leq_subr. rewrite -[p in p %| _](divpK (dvdp_gcdl p q)) exprSr mulrA. by rewrite dvdp_mul ?IHn ?dvdp_gcdr // -ltnS (leq_trans le_d_p). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)