proposition: Lemma real_complex_conjc : forall p : {poly R}, map_poly ((@conjc R) \o (real_complex R)) p = map_poly (real_complex R) p.
proof: Proof. elim/poly_ind => [ | p c H]. by rewrite !rmorph0. by rewrite !rmorphD !rmorphM /= H !map_polyC !map_polyX /= -conjc_real. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype order) mathcomp(prime div bigop ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex)