proposition: Lemma irreducible_dvdp (p : {poly F}) : 1 < size p -> exists2 q : {poly F}, irreducible_poly q & q %| p.
proof: Proof. elim: {p}_.+1 {-2}p (ltnSn (size p)) => // k IH p SpLk Sp_gt1. have [/irreducibleP pI|] := boolP (irreducibleb p); first by exists p. rewrite /irreducibleb Sp_gt1 negb_forall => /existsP[/= q]. rewrite negb_imply -ltnNge => /andP[qDp Sq_gt1]. rewrite -Pdiv.WeakIdomain.dvdpE in qDp. case: (IH _ _ Sq_gt1) => [|r rI rDq]; last first. by exists r => //; apply: dvdp_trans qDp. rewrite -ltnS; apply: leq_ltn_trans SpLk. rewrite -[X in _ < X]prednK ?ltnS; first apply: size_npoly. by apply: leq_ltn_trans Sp_gt1. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)