proposition: Lemma div_annihilantP (p q : {poly E}) (x y : E) : p != 0 -> q != 0 -> y != 0 -> p.[x] = 0 -> q.[y] = 0 -> (div_annihilant p q).[x / y] = 0.
proof: Proof. move=> nz_p nz_q nz_y px0 qy0. have p_gt1: size p > 1 by have /rootP/root_size_gt1-> := px0. have q_gt1: size q > 1 by have /rootP/root_size_gt1-> := qy0. have [uv /= _ /(_ y)->] := div_annihilant_in_ideal p_gt1 q_gt1. by rewrite (mulrC y) divfK // px0 qy0 !mulr0 addr0. 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)