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