proposition: Lemma fpx_resp_deggemonic : forall (f:zx)(n:nat), degree_ge_monic _ n f -> degree_ge_monic _ n (zxfpx f).
proof: Proof. intros f n; unfold degree_ge_monic. intro X; elim X. intros m Hm Hfmonm. exists m. exact Hm. elim Hfmonm. intros Hnthcoeff Hdegf. unfold monic. split. astepl (zfp (nth_coeff m f)). assert ([1][=]nth_coeff m f); intuition. simpl in H. rewrite <- H. intuition. red. intros. astepl (zfp (nth_coeff m0 f)). assert ([0][=]nth_coeff m0 f); intuition. simpl in H0. rewrite <- H0. intuition. Qed.
imports: CoRN.model.Zmod.Zm CoRN.model.rings.Zring CoRN.algebra.CPoly_Degree