proposition: Lemma same_roots_1 : forall (p : {poly R}) (x : R), root p x -> root (divp p (gcdp p p^`())) x.
proof: Proof. move=> p x zero_x. case h: (p==0). by move/eqP: h => H; move : zero_x; rewrite H deriv0 gcd0p div0p. move/negbT: h => H; rewrite -mu_gt0. by move/eqP : (mu_gcdp_eq1 H zero_x) => ->. rewrite divpN0; first by apply: leq_gcdpl. by move/negPf : H => H; rewrite gcdp_eq0 H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype prime) mathcomp(div ssralg poly polydiv polyorder ssrnum zmodp polyrcf)