proposition: Lemma cubic_irreducible p : 1 < size p <= 4 -> (forall x, ~~ root p x) -> irreducible_poly p.
proof: Proof. move=> /andP[p_gt1 p_le4] root'p; split=> // q sz_q_neq1 q_dv_p. have nz_p: p != 0 by rewrite -size_poly_gt0 ltnW. have nz_q: q != 0 by apply: contraTneq q_dv_p => ->; rewrite dvd0p. have q_gt1: size q > 1 by rewrite ltn_neqAle eq_sym sz_q_neq1 size_poly_gt0. rewrite -dvdp_size_eqp // eqn_leq dvdp_leq //= leqNgt; apply/negP=> p_gt_q. by have [|x /idPn//] := reducible_cubic_root p_le4 _ q_dv_p; rewrite q_gt1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)