proposition: Lemma complex_algebraic_trans (T : comRingType) (toR : {rmorphism T -> R}) : integralRange toR -> integralRange (real_complex R \o toR).
proof: Proof. set f := _ \o _ => R_integral [a b]. have integral_real k : integralOver f (k%:C) by apply: integral_rmorph. rewrite [_ +i* _]complexE. apply: integral_add => //; apply: integral_mul => //=. exists ('X^2 + 1). by rewrite monicE lead_coefDl ?size_polyXn ?size_poly1 ?lead_coefXn. by rewrite rmorphD rmorph1 /= ?map_polyXn rootE !hornerE -?expr2 sqr_i addNr. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrint div ssrnum rat poly closed_field) mathcomp(polyrcf matrix mxalgebra tuple mxpoly zmodp binomial realalg) mathcomp(mxpoly)