proposition: Lemma sub_annihilant_neq0 p q : p != 0 -> q != 0 -> sub_annihilant p q != 0.
proof: Proof. rewrite resultant_eq0; set p1 := poly_XaY p => nz_p nz_q. have [nz_p1 nz_q1]: p1 != 0 /\ q^:P != 0 by rewrite poly_XaY_eq0 map_polyC_eq0. rewrite -leqNgt eq_leq //; apply/eqP/Bezout_coprimepPn=> // [[[u v]]] /=. rewrite !size_poly_gt0 -andbA => /and4P[nz_u ltuq nz_v _] Duv. have /eqP/= := congr1 (size \o (lead_coef \o swapXY)) Duv. rewrite ltn_eqF // !rmorphM !lead_coefM (leq_trans (leq_ltn_trans _ ltuq)) //=. rewrite -{2}[u]swapXYK -sizeYE swapXY_poly_XaY lead_coef_poly_XaY. by rewrite mulrC mul_polyC size_scale ?max_size_lead_coefXY ?lead_coef_eq0. rewrite swapXY_map_polyC lead_coefC size_map_polyC. set v1 := lead_coef _; have nz_v1: v1 != 0 by rewrite lead_coef_eq0 swapXY_eq0. rewrite [leqRHS]polySpred ?mulf_neq0 // size_mul //. by rewrite (polySpred nz_v1) addnC addnS polySpred // ltnS leq_addr. 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)