proposition: Lemma same_roots_2 : forall (p : {poly R}) (x : R), root (divp p (gcdp p p^`())) x -> root p x.
proof: Proof. move=> p x zero_x. rewrite -(@rootZ R x (lead_coef (gcdp p p^`()) ^+ scalp (R:=R) p (gcdp p p^`())) p). rewrite -divpK. by rewrite rootM zero_x. by apply dvdp_gcdl. by apply lc_expn_scalp_neq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype prime) mathcomp(div ssralg poly polydiv polyorder ssrnum zmodp polyrcf)