proposition: Lemma reciprocal_toC (p : {poly R}) : toC (@reciprocal_pol _ p) = reciprocal_pol (toC p).
proof: Proof. rewrite /reciprocal_pol poly_def rmorph_sum /= poly_def size_map_inj_poly. - apply: eq_bigr => i _. rewrite -mul_polyC rmorphM /= map_polyXn /=. by rewrite !coef_map /= map_polyC /= mul_polyC. - exact: complexI. - by rewrite -complexr0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)