proposition: Lemma root_annul_from_alg_creal (x : {alg {alg F}}) : ((annul_from_alg (annul_alg x)).[from_alg_creal x] == 0)%CR.
proof: Proof. do 2!apply: eq_to_alg_creal. rewrite -!horner_to_alg_creal from_alg_crealK !to_alg_creal0. rewrite horner_creal_cst; apply/eq_creal_cst; rewrite -rootE. rewrite /annul_from_alg; have [/size_poly1P [c c_neq0 hc]|sp_neq1] := boolP (_ == _). set p := _ ^ _; suff ->: p = (annul_alg x) ^ to_alg _ by apply: root_annul_alg. congr (_ ^ _); rewrite -{2}[annul_alg x]poly_groundK /=. by rewrite !hc lead_coefC map_polyC /= hornerC. have [||[u v] /= [hu hv] hpq] := @resultant_in_ideal _ (poly_ground (annul_alg x)) (annul_pet_alg (annul_alg x) ^ polyC). + rewrite ltn_neqAle eq_sym sp_neq1 //= lt0n size_poly_eq0. by rewrite poly_ground_eq0 annul_alg_neq0. + rewrite size_map_polyC -(size_map_poly [rmorphism of to_alg _]) /=. rewrite (root_size_gt1 _ (root_annul_pet_alg _)) //. by rewrite map_poly_eq0 annul_pet_alg_neq0 ?annul_alg_neq0. move: hpq=> /(f_equal (map_poly (map_poly (to_alg _)))). rewrite map_polyC /= => /(f_equal (eval (pet_alg (annul_alg x))%:P)). rewrite {1}/eval hornerC !rmorphD !{1}rmorphM /= /eval /= => ->. rewrite -map_poly_comp /=. have /eq_map_poly->: (map_poly (@to_alg F)) \o polyC =1 polyC \o (@to_alg F). by move=> r /=; rewrite map_polyC. rewrite map_poly_comp horner_map /= (rootP (root_annul_pet_alg _)) mulr0 addr0. by rewrite rmorphM /= rootM orbC poly_groundK root_annul_alg. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial generic_quotient) mathcomp(cauchyreals separable zmodp bigenough)