proposition: Lemma reciprocal_monom (a b: R): a != 0 -> reciprocal_pol ('X * a%:P + b%:P) = ('X * b%:P + a%:P).
proof: Proof. move=> /negbTE h; rewrite /reciprocal_pol. have ->: size ('X * a%:P + b%:P) = 2%N. by rewrite - commr_polyX size_MXaddC size_polyC polyC_eq0 h. apply/polyP=> i. rewrite coef_poly !coefD !coefMC !coefC !coefX. case :i; first by rewrite mul1r mul0r add0r addr0. case; first by rewrite mul1r mul0r add0r addr0. by move=> n /=; rewrite mul0r add0r. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)