proposition: Lemma root_gcd p q x : root (gcdp p q) x = root p x && root q x.
proof: Proof. rewrite /= !root_factor_theorem; apply/idP/andP=> [dg| [dp dq]]. by split; apply: dvdp_trans dg _; rewrite ?(dvdp_gcdl, dvdp_gcdr). have:= Bezoutp p q => [[[u v]]]; rewrite eqp_sym=> e. by rewrite (eqp_dvdr _ e) dvdp_addl dvdp_mull. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)