proposition: Lemma map_sub_annihilantP (p q : {poly F}) (x y : E) : p != 0 -> q != 0 ->(p ^ FtoE).[x] = 0 -> (q ^ FtoE).[y] = 0 -> (sub_annihilant p q ^ FtoE).[x - y] = 0.
proof: Proof. move=> nz_p nz_q px0 qy0; have pFto0 := map_poly_eq0 FtoE. rewrite map_resultant ?pFto0 ?lead_coef_eq0 ?map_poly_eq0 ?poly_XaY_eq0 //. rewrite map_comp_poly rmorphD /= map_polyC /= !map_polyX -!map_poly_comp /=. by rewrite !(eq_map_poly (map_polyC _)) !map_poly_comp sub_annihilantP ?pFto0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype tuple finfun bigop fingroup perm div) mathcomp(ssralg zmodp matrix mxalgebra) mathcomp(poly polydiv mxpoly binomial)