proposition: Lemma annul_from_alg_proof (p : {poly alg}) (q : {poly F}) : p != 0 -> q != 0 -> root (q ^ to_alg) (pet_alg p) -> {r | resultant (poly_ground p) (r ^ polyC) != 0 & (r != 0) && (root (r ^ to_alg) (pet_alg p))}.
proof: Proof. move=> p_neq0; elim: (size q) {-2}q (leqnn (size q))=> {q} [|n ihn] q. by rewrite size_poly_leq0=> ->. move=> size_q q_neq0 hq; apply/sig2_eqW. have [|apq_neq0] := eqVneq (resultant (poly_ground p) (q ^ polyC)) 0; last first. by exists q=> //; rewrite q_neq0. move/eqP; rewrite resultant_eq0 ltn_neqAle eq_sym -coprimep_def. move=> /andP[] /(Bezout_coprimepPn _ _) []. + by rewrite poly_ground_eq0. + by rewrite map_polyC_eq0. move=> [u v] /and3P [] /andP [u_neq0 ltn_uq] v_neq0 ltn_vp hpq. rewrite ?size_map_polyC in ltn_uq ltn_vp. rewrite ?size_poly_gt0 in u_neq0 v_neq0. pose a := pet_alg p. have := erefl (size ((u * poly_ground p) ^ (map_poly to_alg)).[a%:P]). rewrite {2}hpq !{1}rmorphM /= !{1}hornerM poly_groundK -map_poly_comp /=. have /eq_map_poly-> : (map_poly to_alg) \o polyC =1 polyC \o to_alg. by move=> r /=; rewrite map_polyC. rewrite map_poly_comp horner_map (rootP hq) mulr0 size_poly0. move/eqP; rewrite size_poly_eq0 mulf_eq0 (negPf p_neq0) orbF. pose u' : {poly F} := lead_coef (swapXY u). have [/rootP u'a_eq0|u'a_neq0] := eqVneq (u' ^ to_alg).[a] 0; last first. rewrite horner_polyC -lead_coef_eq0 lead_coef_map_eq /=; by do ?rewrite swapXY_map /= lead_coef_map_eq /= ?map_poly_eq0 ?lead_coef_eq0 ?swapXY_eq0 ?(negPf u'a_neq0). have u'_neq0 : u' != 0 by rewrite lead_coef_eq0 swapXY_eq0. have size_u' : (size u' < size q)%N. by rewrite /u' (leq_ltn_trans (max_size_lead_coefXY _)) // sizeYE swapXYK. move: u'a_eq0=> /ihn [] //; first by rewrite -ltnS (leq_trans size_u'). by move=> r; exists r. 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)