proposition: Lemma dvdp_size_eqp p q : p %| q -> size p == size q = (p %= q).
proof: Proof. move=> pq; apply/idP/idP; last by move/eqp_size->. have [->|Hq] := eqVneq q 0; first by rewrite size_poly0 size_poly_eq0 eqp0. have [->|Hp] := eqVneq p 0. by rewrite size_poly0 eq_sym size_poly_eq0 eqp_sym eqp0. move: pq; rewrite dvdp_eq; set c := _ ^+ _; set x := _ %/ _; move/eqP=> eqpq. have /= := congr1 (size \o @polyseq R) eqpq. have cn0 : c != 0 by rewrite expf_neq0 // lead_coef_eq0. rewrite (@eqp_size _ q); last exact: eqp_scale. rewrite size_mul ?p0 // => [-> HH|]; last first. apply/eqP=> HH; move: eqpq; rewrite HH mul0r. by move/eqP; rewrite scale_poly_eq0 (negPf Hq) (negPf cn0). suff: size x == 1%N. case/size_poly1P=> y H1y H2y. by apply/eqpP; exists (y, c); rewrite ?H1y // eqpq H2y mul_polyC. case: (size p) HH (size_poly_eq0 p)=> [|n]; first by case: eqP Hp. by rewrite addnS -add1n eqn_add2r; move/eqP->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)