proposition: Lemma pdivmu0_0th_neq0 (p : {poly R}) : p != 0 -> (p %/ 'X^(\mu_0 p))`_0 != 0.
proof: Proof. move=> Hp. have H0noroot : ~~(root (p %/ 'X^(\mu_0 p)) 0). rewrite -mu_gt0. rewrite -eqn0Ngt -(addr0 'X) -(@oppr0 (poly_zmodType R)) -polyC0 mu_div ?subn_eq0; by rewrite leqnn. rewrite Pdiv.CommonIdomain.divp_eq0 negb_or Hp /= negb_or. rewrite -size_poly_gt0 {1}size_polyXn /= -leqNgt dvdp_leq //. by rewrite -(addr0 'X) -oppr0 -polyC0 root_mu. rewrite -horner_coef0. apply: negbT. by move/rootPf : H0noroot. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)