proposition: Lemma cpoly_lin_plus_lin : forall p q c d, cpoly_plus_cs (cpoly_linear_cs c p) (cpoly_linear_cs d q) = cpoly_linear_cs (c[+]d) (cpoly_plus_cs p q).
proof: Proof. auto. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational