proposition: Lemma size2_dvdp_gdco p q d : p != 0 -> size d = 2 -> (d %| (gdcop q p)) = (d %| p) && ~~(d %| q).
proof: Proof. have [-> | dn0] := eqVneq d 0; first by rewrite size_poly0. move=> p0 sd; apply/idP/idP. case: gdcopP=> r rp crq maxr dr; move/negPf: (p0)=> p0f. rewrite (dvdp_trans dr) //=. apply: contraL crq => dq; rewrite p0f orbF; apply/coprimepPn. by apply: contraNneq p0 => r0; move: rp; rewrite r0 dvd0p. by exists d; rewrite dvdp_gcd dr dq -size_poly_eq1 sd. case/andP=> dp dq; case: gdcopP=> r rp crq maxr; apply: maxr=> //. apply/coprimepP=> x xd xq. move: (dvdp_leq dn0 xd); rewrite leq_eqVlt sd; case/orP; last first. rewrite ltnS leq_eqVlt ltnS size_poly_leq0 orbC. case/predU1P => [x0|]; last by rewrite -size_poly_eq1. by move: xd; rewrite x0 dvd0p (negPf dn0). by rewrite -sd dvdp_size_eqp //; move/(eqp_dvdl q); rewrite xq (negPf dq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)