proposition: Lemma smaller_factor (p q : {poly F}) x : p \is monic-> p.[x] == 0 -> ~~(p %| q) -> ~~ coprimep p q -> {r : {poly F} | (size r < size p)%N && (r \is monic) & r.[x] == 0}.
proof: Proof. move=> monic_p px0 ndvd_pq. rewrite /coprimep; set d := gcdp _ _=> sd_neq1. pose r1 : {poly F} := (lead_coef d)^-1 *: d. pose r2 := p %/ r1. have ld_neq0 : lead_coef d != 0 :> F. by rewrite lead_coef_eq0 gcdp_eq0 negb_and monic_neq0. have monic_r1 : r1 \is monic. by rewrite monicE /r1 -mul_polyC lead_coefM lead_coefC mulVf. have eq_p_r2r1: p = r2 * r1. by rewrite divpK // (@eqp_dvdl _ d) ?dvdp_gcdl // eqp_scale ?invr_eq0. have monic_r2 : r2 \is monic by rewrite -(monicMr _ monic_r1) -eq_p_r2r1. have eq_sr1_sd : size r1 = size d by rewrite size_scale ?invr_eq0. have sr1 : (1 < size r1)%N. by rewrite ltn_neqAle eq_sym lt0n size_poly_eq0 monic_neq0 ?andbT ?eq_sr1_sd. have sr2 : (1 < size r2)%N. rewrite size_divp ?size_dvdp ?monic_neq0 //. rewrite ltn_subRL addn1 prednK ?(leq_trans _ sr1) // eq_sr1_sd. rewrite ltn_neqAle dvdp_leq ?monic_neq0 ?andbT ?dvdp_size_eqp ?dvdp_gcdl //. by apply: contra ndvd_pq=> /eqp_dvdl <-; rewrite dvdp_gcdr. move: (px0); rewrite eq_p_r2r1=> r2r1x_eq0. have : (r2.[x] * r1.[x] == 0) by rewrite -horner_crealM. case/poly_mul_creal_eq0=> [r2x_eq0|r1x_eq0]. exists r2; rewrite ?monic_r2 ?andbT // mulrC. by rewrite -ltn_divpl ?divpp ?monic_neq0 // size_poly1. exists r1; rewrite ?monic_r1 ?andbT //. by rewrite -ltn_divpl ?divpp ?monic_neq0 // size_poly1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)