proposition: Lemma fpx_resp_red : forall f:zx, (reducible _ f)->(reducible fp (zxfpx f)).
proof: Proof. intros f Hfred; elim Hfred. intros Hfok Hfred2; elim Hfred2. intros g Hgok Hfred3; elim Hfred3. intros h Hhok Hfgh; unfold reducible. intuition. exists (zxfpx g). intuition. exists (zxfpx h). intuition. astepr (zxfpx (cpoly_mult_op _ g h)). apply fpxeq_wd. exact Hfgh. Qed.
imports: CoRN.model.Zmod.Zm CoRN.model.rings.Zring CoRN.algebra.CPoly_Degree