proposition: Theorem irrcrit : forall f:zx, (irreducible fp (zxfpx f)) -> (irreducible _ f).
proof: Proof. unfold irreducible. intro f. cut ((reducible _ f) -> (reducible fp (zxfpx f))). intros X H X0. apply H. apply X. exact X0. apply fpx_resp_red. Qed.
imports: CoRN.model.Zmod.Zm CoRN.model.rings.Zring CoRN.algebra.CPoly_Degree