proposition: Lemma sub_annihilant_in_ideal p q : 1 < size p -> 1 < size q -> {uv : {poly {poly R}} * {poly {poly R}} | size uv.1 < size q /\ size uv.2 < size p & forall x y, (sub_annihilant p q).[y] = uv.1.[x, y] * p.[x + y] + uv.2.[x, y] * q.[x]}.
proof: Proof. rewrite -size_poly_XaY -(size_map_polyC q) => p1_gt1 q1_gt1. have [uv /= [ub_u ub_v Dr]] := resultant_in_ideal p1_gt1 q1_gt1. exists uv => // x y; rewrite -[r in r.[y]](hornerC _ x%:P) Dr. by rewrite !(hornerE, horner_comp). 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)