proposition: Lemma cpoly_lin_mult_cr : forall c d q, cpoly_mult_cr_cs (cpoly_linear_cs d q) c = cpoly_linear_cs (c[*]d) (cpoly_mult_cr_cs q c).
proof: Proof. auto. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational