proposition: Lemma cpoly_plus_op_wd : bin_op_wd cpoly_csetoid cpoly_plus_cs.
proof: Proof. unfold bin_op_wd in |- *. apply bin_fun_strext_imp_wd. exact cpoly_plus_op_strext. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational