proposition: Lemma resultant_in_ideal (R : comRingType) (p q : {poly R}) : size p > 1 -> size q > 1 -> {uv : {poly R} * {poly R} | size uv.1 < size q /\ size uv.2 < size p & (resultant p q)%:P = uv.1 * p + uv.2 * q}.
proof: Proof. move=> p_nc q_nc; pose dp := (size p).-1; pose dq := (size q).-1. pose S := Sylvester_mx p q; pose dS := (dq + dp)%N. have dS_gt0: dS > 0 by rewrite /dS /dq -(subnKC q_nc). pose j0 := Ordinal dS_gt0. pose Ss0 := col_mx (p *: \col_(i < dq) 'X^i) (q *: \col_(i < dp) 'X^i). pose Ss := \matrix_(i, j) (if j == j0 then Ss0 i 0 else (S i j)%:P). pose u ds s := \sum_(i < ds) cofactor Ss (s i) j0 * 'X^i. exists (u _ (lshift dp), u _ ((rshift dq) _)). suffices sz_u ds s: ds > 1 -> size (u ds.-1 s) < ds by rewrite !sz_u. move/ltn_predK=> {2}<-; apply: leq_trans (size_sum _ _ _) _. apply/bigmax_leqP=> i _. have ->: cofactor Ss (s i) j0 = (cofactor S (s i) j0)%:P. rewrite rmorphM /= rmorph_sign -det_map_mx; congr (_ * \det _). by apply/matrixP=> i' j'; rewrite !mxE. apply: leq_trans (size_mul_leq _ _) (leq_trans _ (valP i)). by rewrite size_polyC size_polyXn addnS /= -add1n leq_add2r leq_b1. transitivity (\det Ss); last first. rewrite (expand_det_col Ss j0) big_split_ord !big_distrl /=. by congr (_ + _); apply: eq_bigr => i _; rewrite mxE eqxx (col_mxEu, col_mxEd) !mxE mulrC mulrA mulrAC. pose S_ j1 := map_mx polyC (\matrix_(i, j) S i (if j == j0 then j1 else j)). pose Ss0_ i dj := \poly_(j < dj) S i (insubd j0 j). pose Ss_ dj := \matrix_(i, j) (if j == j0 then Ss0_ i dj else (S i j)%:P). have{Ss u} ->: Ss = Ss_ dS. apply/matrixP=> i j; rewrite mxE [in RHS]mxE; case: (j == j0) => {j}//. apply/polyP=> k; rewrite coef_poly Sylvester_mxE mxE. have [k_ge_dS | k_lt_dS] := leqP dS k. case: (split i) => {}i; rewrite !mxE coefMXn; case: ifP => // /negbT; rewrite -ltnNge ltnS => hi. apply: (leq_sizeP _ _ (leqnn (size p))); rewrite -(ltn_predK p_nc). by rewrite ltn_subRL (leq_trans _ k_ge_dS) // ltn_add2r. - apply: (leq_sizeP _ _ (leqnn (size q))); rewrite -(ltn_predK q_nc). by rewrite ltn_subRL (leq_trans _ k_ge_dS) // addnC ltn_add2l. by rewrite insubdK //; case: (split i) => {}i; rewrite !mxE coefMXn; case: leqP. case: (ubnPgeq dS) (dS_gt0); elim=> // dj IHj ltjS _; pose j1 := Ordinal ltjS. pose rj0T (A : 'M[{poly R}]_dS) := row j0 A^T. have: rj0T (Ss_ dj.+1) = 'X^dj *: rj0T (S_ j1) + 1 *: rj0T (Ss_ dj). apply/rowP=> i; apply/polyP=> k; rewrite scale1r !(Sylvester_mxE, mxE) eqxx. rewrite coefD coefXnM coefC !coef_poly ltnS subn_eq0 ltn_neqAle andbC. have [k_le_dj | k_gt_dj] /= := leqP k dj; last by rewrite addr0. rewrite Sylvester_mxE insubdK; last exact: leq_ltn_trans (ltjS). by have [->|] := eqP; rewrite (addr0, add0r). rewrite -det_tr => /determinant_multilinear->; try by apply/matrixP=> i j; rewrite !mxE lift_eqF. have [dj0 | dj_gt0] := posnP dj; rewrite ?dj0 !mul1r. rewrite !det_tr det_map_mx addrC (expand_det_col _ j0) big1 => [|i _]. rewrite add0r; congr (\det _)%:P. apply/matrixP=> i j; rewrite [in RHS]mxE; case: eqP => // ->. by congr (S i _); apply: val_inj. by rewrite mxE /= [Ss0_ _ _]poly_def big_ord0 mul0r. have /determinant_alternate->: j1 != j0 by rewrite -val_eqE -lt0n. by rewrite mulr0 add0r det_tr IHj // ltnW. by move=> i; rewrite !mxE if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)