proposition: Lemma gcdp_simple_roots : forall (p : {poly R}) (x : R), (p != 0) -> root (divp p (gcdp p p^`())) x -> (\mu_x (divp p (gcdp p p^`())) == 1)%N.
proof: Proof. by move=> p x Hp zero_x; apply (mu_gcdp_eq1 Hp); apply same_roots_2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype prime) mathcomp(div ssralg poly polydiv polyorder ssrnum zmodp polyrcf)