proposition: Lemma cpoly_const_plus : forall a b : R, cpoly_constant_fun _ (a[+]b) [=] cpoly_constant_fun _ a[+]cpoly_constant_fun _ b.
proof: Proof. simpl in |- *; split; algebra. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational