proposition: Lemma fpx_resp_mult_cr : forall (c:Z_as_CRing)(f:zx), (cpoly_mult_cr_cs fp (zxfpx f) (zfp c)) [=] (zxfpx (cpoly_mult_cr_cs _ f c)).
proof: Proof. induction f as [|c0 f]. intuition. astepr (zxfpx ((c[*]c0)[+X*](cpoly_mult_cr_cs _ f c))). astepr ((zfp (c[*]c0))[+X*](zxfpx (cpoly_mult_cr_cs _ f c))). astepr (((zfp c)[*](zfp c0))[+X*](zxfpx (cpoly_mult_cr_cs _ f c))). astepr (((zfp c)[*](zfp c0))[+X*](cpoly_mult_cr_cs fp (zxfpx f) (zfp c))). astepr (cpoly_mult_cr_cs fp ((zfp c0)[+X*](zxfpx f)) (zfp c)). intuition. Qed.
imports: CoRN.model.Zmod.Zm CoRN.model.rings.Zring CoRN.algebra.CPoly_Degree