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