proposition: Lemma reciprocalX p n : reciprocal_pol (p ^+ n) = (reciprocal_pol p) ^+ n.
proof: Proof. elim: n=> [| n Hrec]; first rewrite !expr0 reciprocalC //. by rewrite ! exprS reciprocalM Hrec. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)