proposition: Lemma Ccpoly_ind_cs : forall P : cpoly_csetoid -> CProp, P cpoly_zero_cs -> (forall p c, P p -> P (cpoly_linear_cs c p)) -> forall p, P p.
proof: Proof. simple induction p; auto. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational