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