proposition: Lemma fpxeq_wd : forall f g:zx, f[=]g -> (zxfpx f)[=](zxfpx g).
proof: Proof. apply (cpoly_double_ind Z_as_CRing P); unfold P. induction p0 as [|c p0]. trivial. intro H. astepl ((zfp c)[+X*](zxfpx p0)). apply (_linear_eq_zero fp). split. astepr (zfp 0). apply fpeq_wd. elim H. auto. apply IHp0. elim H. auto with *. induction p0 as [|c p0]. trivial. intro H. astepr ((zfp c)[+X*](zxfpx p0)). apply (_zero_eq_linear fp). split. astepr (zfp 0). apply fpeq_wd. elim H. auto. apply IHp0. elim H. auto with *. intros p0 q c d H1 H2. astepr ((zfp d)[+X*](zxfpx q)). astepl ((zfp c)[+X*](zxfpx p0)). apply (_linear_eq_linear fp). split. apply fpeq_wd. elim H2. auto. apply H1. elim H2. auto. Qed.
imports: CoRN.model.Zmod.Zm CoRN.model.rings.Zring CoRN.algebra.CPoly_Degree