proposition: Lemma fpx_resp_mult : forall f g:zx, (cpoly_mult_op fp (zxfpx f) (zxfpx g)) [=] (zxfpx (cpoly_mult_op _ f g)).
proof: Proof. induction f as [|c f]. intro g. astepl (cpoly_mult_op fp (cpoly_zero fp)(zxfpx g)). astepl (cpoly_zero fp). astepr (zxfpx (cpoly_zero Z_as_CRing)). astepr (cpoly_zero fp); intuition. induction g as [|c0 g]. astepl (cpoly_mult_op fp (zxfpx (c[+X*]f)) (cpoly_zero fp)). astepl (cpoly_zero fp). astepr (zxfpx (cpoly_zero Z_as_CRing)); try algebra. apply fpxeq_wd. apply eq_symmetric. apply (mult_zero Z_as_CRing). astepr (zxfpx (cpoly_mult_op Z_as_CRing (c[+X*]f) (c0[+X*]g))). astepl (cpoly_mult_op fp (zxfpx (c[+X*]f)) (zxfpx (c0[+X*]g))). astepr (zxfpx (cpoly_plus_op _ ((c[*]c0)[+X*](cpoly_mult_cr_cs _ g c)) (([0]:Z_as_CRing)[+X*](cpoly_mult _ f (c0[+X*]g))))). astepr (zxfpx (((c[*]c0)[+]([0]:Z_as_CRing))[+X*](cpoly_plus_op _ (cpoly_mult_cr_cs _ g c) (cpoly_mult _ f (c0[+X*]g))))). astepr (zxfpx ((c[*]c0)[+X*](cpoly_plus_op _ (cpoly_mult_cr_cs _ g c) (cpoly_mult _ f (c0[+X*]g))))). astepr ( (zfp c[*]c0) [+X*] (zxfpx (cpoly_plus_op _ (cpoly_mult_cr_cs _ g c) (cpoly_mult _ f (c0[+X*]g))))). astepl (cpoly_mult_op fp ((zfp c)[+X*](zxfpx f)) (zxfpx (c0[+X*]g))). astepl (cpoly_plus_op fp (cpoly_mult_cr_cs fp (zxfpx (c0[+X*]g)) (zfp c)) ((zfp ([0]:Z_as_CRing))[+X*](cpoly_mult_op fp (zxfpx f) (zxfpx (c0[+X*]g))))). astepl (cpoly_plus_op fp (cpoly_mult_cr_cs fp ((zfp c0)[+X*](zxfpx g)) (zfp c)) (([0]:fp)[+X*](zxfpx (cpoly_mult_op _ f (c0[+X*]g))))). astepl (cpoly_plus_op fp (((zfp c)[*](zfp c0))[+X*](cpoly_mult_cr_cs fp (zxfpx g) (zfp c))) (([0]:fp)[+X*](zxfpx (cpoly_mult_op _ f (c0[+X*]g))))). astepl (cpoly_plus_op fp ((zfp (c[*]c0))[+X*](zxfpx (cpoly_mult_cr_cs _ g c))) (([0]:fp)[+X*](zxfpx (cpoly_mult_op _ f (c0[+X*]g))))). astepl ((zfp (c[*]c0)[+]([0]:fp))[+X*](cpoly_plus_op fp (zxfpx (cpoly_mult_cr_cs _ g c)) (zxfpx (cpoly_mult_op _ f (c0[+X*]g))))). intuition. Qed.
imports: CoRN.model.Zmod.Zm CoRN.model.rings.Zring CoRN.algebra.CPoly_Degree