fact: Fixpoint in_coeff (c : R) (p : RX) {struct p} : Prop := match p with | cpoly_zero => False | cpoly_linear d q => c [=] d \/ in_coeff c q end.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings