proposition: Lemma subfx_irreducibleP : (forall q, root q^iota z -> q != 0 -> size p <= size q) <-> irreducible_poly p.
proof: Proof. split=> [min_p | irr_p q qz0 nz_q]. split=> [|q nonC_q q_dv_p]. by rewrite -(size_map_poly iota) (root_size_gt1 _ pz0) ?map_poly_eq0. have /dvdpP[r Dp] := q_dv_p; rewrite -dvdp_size_eqp // eqn_leq dvdp_leq //=. have [nz_r nz_q]: r != 0 /\ q != 0 by apply/norP; rewrite -mulf_eq0 -Dp. have: root r^iota z || root q^iota z by rewrite -rootM -rmorphM -Dp. case/orP=> /min_p; [case/(_ _)/idPn=> // | exact]. rewrite polySpred // -leqNgt Dp size_mul //= polySpred // -subn2 ltn_subRL. by rewrite addSnnS addnC ltn_add2l ltn_neqAle eq_sym nonC_q size_poly_gt0. pose r := gcdp p q; have nz_r: r != 0 by rewrite gcdp_eq0 (negPf nz_p). suffices /eqp_size <-: r %= p by rewrite dvdp_leq ?dvdp_gcdr. rewrite (irr_p _) ?dvdp_gcdl // -(size_map_poly iota) gtn_eqF //. by rewrite (@root_size_gt1 _ z) ?map_poly_eq0 // gcdp_map root_gcd pz0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg countalg) mathcomp(finalg zmodp matrix vector falgebra poly polydiv) mathcomp(mxpoly generic_quotient)