proposition: Lemma cpoly_lin_mult : forall c p q, cpoly_mult_cs (cpoly_linear_cs c p) q = cpoly_plus_cs (cpoly_mult_cr_cs q c) (cpoly_linear_cs [0] (cpoly_mult_cs p q)).
proof: Proof. auto. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational