proposition: Lemma div_annihilant_neq0 p q : p != 0 -> q.[0] != 0 -> div_annihilant p q != 0.
proof: Proof. have factorX u: u != 0 -> root u 0 -> exists2 v, v != 0 & u = v * 'X. move=> nz_u /factor_theorem[v]; rewrite subr0 => Du; exists v => //. by apply: contraNneq nz_u => v0; rewrite Du v0 mul0r. have nzX: 'X != 0 := monic_neq0 (monicX _); have rootC0 := root_polyC _ 0. rewrite resultant_eq0 -leqNgt -rootE // => nz_p nz_q0; apply/eq_leq/eqP. have nz_q: q != 0 by apply: contraNneq nz_q0 => ->; rewrite root0. apply/Bezout_coprimepPn; rewrite ?map_polyC_eq0 ?poly_XmY_eq0 // => [[uv]]. rewrite !size_poly_gt0 -andbA ltnNge => /and4P[nz_u /negP ltuq nz_v _] Duv. pose u := swapXY uv.1; pose v := swapXY uv.2. suffices{ltuq}: size q <= sizeY u by rewrite sizeYE swapXYK -size_map_polyC. have{nz_u nz_v} [nz_u nz_v Dvu]: [/\ u != 0, v != 0 & q *: v = u * poly_XmY p]. rewrite !swapXY_eq0; split=> //; apply: (can_inj swapXYK). by rewrite linearZ rmorphM /= !swapXYK swapXY_poly_XmY Duv mulrC. have{Duv} [n ltvn]: {n | size v < n} by exists (size v).+1. elim: n {uv} => // n IHn in p (v) (u) nz_u nz_v Dvu nz_p ltvn *. have Dp0: root (poly_XmY p) 0 = root p 0 by rewrite root_comp !hornerE rootC0. have Dv0: root u 0 || root p 0 = root v 0 by rewrite -Dp0 -rootM -Dvu rootZ. have [v0_0 | nz_v0] := boolP (root v 0); last first. have nz_p0: ~~ root p 0 by apply: contra nz_v0; rewrite -Dv0 orbC => ->. apply: (@leq_trans (size (q * v.[0]))). by rewrite size_mul // (polySpred nz_v0) addnS leq_addr. rewrite -hornerZ Dvu !(horner_comp, hornerE) horner_map mulrC size_Cmul //. by rewrite horner_coef0 max_size_coefXY. have [v1 nz_v1 Dv] := factorX _ _ nz_v v0_0; rewrite Dv size_mulX // in ltvn. have /orP[/factorX[//|u1 nz_u1 Du] | p0_0]: root u 0 || root p 0 by rewrite Dv0. rewrite Du sizeY_mulX; apply: IHn nz_u1 nz_v1 _ nz_p ltvn. by apply: (mulIf (nzX _)); rewrite mulrAC -scalerAl -Du -Dv. have /factorX[|v2 nz_v2 Dv1]: root (swapXY v1) 0; rewrite ?swapXY_eq0 //. suffices: root (swapXY v1 * 'Y) 0 by rewrite mulrC mul_polyC rootZ ?polyX_eq0. have: root (swapXY (q *: v)) 0. by rewrite Dvu rmorphM rootM /= swapXY_poly_XmY Dp0 p0_0 orbT. by rewrite linearZ rootM rootC0 (negPf nz_q0) /= Dv rmorphM /= swapXY_X. rewrite ltnS (canRL swapXYK Dv1) -sizeYE sizeY_mulX sizeYE in ltvn. have [p1 nz_p1 Dp] := factorX _ _ nz_p p0_0. apply: IHn nz_u _ _ nz_p1 ltvn; first by rewrite swapXY_eq0. have: 'X * 'Y != 0 :> {poly {poly R}} by rewrite mulf_neq0 ?polyC_eq0 ?nzX. move/mulIf; apply. rewrite -scalerAl mulrA mulrAC -{1}swapXY_X -rmorphM /= -Dv1 swapXYK -Dv Dvu. by rewrite /poly_XmY Dp rmorphM /= map_polyX comp_polyM comp_polyX mulrA. 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)