proposition: Lemma cpoly_lin_ap_zero_ : forall p c, cpoly_linear_cs c p [#] cpoly_zero_cs -> c [#] [0] or p [#] cpoly_zero_cs.
proof: Proof. unfold cpoly_zero_cs in |- *. intros p c H. cut (cpoly_ap (cpoly_linear c p) cpoly_zero); auto. intro H0. simpl in H0. elim H0; auto. right. rewrite <- cpoly_ap_p_zero. assumption. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational