proposition: Lemma irreducibleP : reflect (irreducible_poly p) irreducibleb.
proof: Proof. rewrite /irreducibleb /irreducible_poly. apply: (iffP idP) => [/andP[sp /'forall_implyP /= Fp]|[sp Fpoly]]. have sp_gt0 : size p > 0 by case: size sp. have p_neq0 : p != 0 by rewrite -size_poly_eq0; case: size sp. split => // q sq_neq1 dvd_qp; rewrite -dvdp_size_eqp // eqn_leq dvdp_leq //=. apply: contraNT sq_neq1; rewrite -ltnNge => sq_lt_sp. have q_small: (size q <= (size p).-1)%N by rewrite -ltnS prednK. rewrite Pdiv.Idomain.dvdpE in dvd_qp. have /= := Fp (Npolynomial q_small) dvd_qp. rewrite leq_eqVlt ltnS => /orP[//|]; rewrite size_poly_leq0 => /eqP q_eq0. by rewrite -Pdiv.Idomain.dvdpE q_eq0 dvd0p (negPf p_neq0) in dvd_qp. have sp_gt0 : size p > 0 by case: size sp. rewrite sp /=; apply/'forall_implyP => /= q; rewrite -Pdiv.Idomain.dvdpE=> dvd_qp. have [/eqP->//|/Fpoly/(_ dvd_qp)/eqp_size sq_eq_sp] := boolP (sizep q == 1%N). by have := size_npoly q; rewrite sq_eq_sp -ltnS prednK ?ltnn. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop binomial finset finfun zmodp ssralg countalg finalg poly polydiv) mathcomp(perm fingroup) CoqEAL(hrel pos param refinements binnat boolF2 seqpoly poly_op trivial_seq poly_div boolF2)