proposition: Lemma reciprocal_Xn_root0 (p : {poly R}) : reciprocal_pol p = reciprocal_pol (p %/ 'X^(\mu_0 p)).
proof: Proof. rewrite -(addr0 'X) -oppr0. have Hmu0 := root_mu p 0. rewrite Pdiv.IdomainMonic.dvdp_eq in Hmu0; last first. by rewrite monic_exp// monicXsubC. by rewrite {1}(eqP Hmu0) reciprocalM {2}oppr0 addr0 reciprocal_Xn polyC1 mulr1 polyC0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)