proposition: Lemma fpx_resp_plus : forall f g:zx, (cpoly_plus_op fp (zxfpx f) (zxfpx g))[=] (zxfpx (cpoly_plus_op _ f g)).
proof: Proof. induction f as [|c f]. intuition. induction g as [|c0 g]. intuition. astepl (cpoly_plus fp (zxfpx (c[+X*]f)) (zxfpx (c0[+X*]g))). astepr (zxfpx (cpoly_plus_op _ (c[+X*]f) (c0[+X*]g))). astepr (zxfpx ((c[+]c0)[+X*](cpoly_plus_op _ f g))). astepr ((zfp (c[+]c0))[+X*](zxfpx (cpoly_plus_op _ f g))). astepl (((zfp c)[+](zfp c0))[+X*] (cpoly_plus_op fp (zxfpx f) (zxfpx g))). auto with *. Qed.
imports: CoRN.model.Zmod.Zm CoRN.model.rings.Zring CoRN.algebra.CPoly_Degree