fact: Fixpoint cpoly_mult_cr (q : cpoly) (c : CR) {struct q} : cpoly := match q with | cpoly_zero => cpoly_zero | cpoly_linear d q1 => cpoly_linear (c[*]d) (cpoly_mult_cr q1 c) end.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational