proposition: Lemma reciprocalC (c : R) : reciprocal_pol c%:P = c%:P.
proof: Proof. rewrite /reciprocal_pol - polyP => i; rewrite coef_poly. case cz: (c==0); first by move /eqP in cz; rewrite cz !coef0 if_same. rewrite size_polyC cz !coefC; case:i => [| i]//. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)