proposition: Lemma mult_zero : forall (R:CRing)(f:cpoly_cring R), (cpoly_mult_op R f (cpoly_zero R))[=](cpoly_zero R).
proof: Proof. intros R f. simpl; apply cpoly_mult_zero. Qed.
imports: CoRN.model.Zmod.Zm CoRN.model.rings.Zring CoRN.algebra.CPoly_Degree