proposition: Lemma root_gdco p q x : p != 0 -> root (gdcop q p) x = root p x && ~~(root q x).
proof: Proof. move=> p0 /=; rewrite !root_factor_theorem. apply: size2_dvdp_gdco; rewrite ?p0 //. by rewrite size_addl size_polyX // size_opp size_polyC ltnS; case: (x != 0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)