proposition: Lemma _cpoly_zero_ap_lin : forall p c, c [#] [0] or cpoly_zero_cs [#] p -> cpoly_zero_cs [#] cpoly_linear_cs c p.
proof: Proof. intros. simpl in |- *. assumption. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational