proposition: Lemma reciprocal_reciprocal (p : {poly R}) : reciprocal_pol (reciprocal_pol p) = p %/ ('X^(\mu_0 p)).
proof: Proof. case Hp0 : (p == 0). move/eqP : Hp0 => ->. by rewrite !reciprocalC div0p polyC0. rewrite (@reciprocal_Xn_root0 p) reciprocal_idempotent //. apply: pdivmu0_0th_neq0. by apply: negbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)