proposition: Lemma reciprocal0 (p : {poly R}) : (reciprocal_pol p == 0) = (p == 0).
proof: Proof. apply/idP/idP => Hp. have H : (p %/ ('X^(\mu_0 p)) == 0). by rewrite -reciprocal_reciprocal -polyC0 -reciprocalC (eqP Hp). rewrite Pdiv.CommonIdomain.divp_eq0 in H. move/orP : H; case => [| /orP [] H] //. by rewrite -size_poly_eq0 size_polyXn -(Bool.negb_involutive (_.+1 == 0%N)) -lt0n /= in H. have H2 := (root_mu p 0). case Hp0 : (p == 0) => //. rewrite gtNdvdp // in H2. by apply: negbT. by rewrite oppr0 addr0. by rewrite (eqP Hp) -polyC0 reciprocalC. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)