proposition: Lemma _cpoly_lin_ap_zero : forall p c, c [#] [0] or p [#] cpoly_zero_cs -> cpoly_linear_cs c p [#] cpoly_zero_cs.
proof: Proof. unfold cpoly_zero_cs in |- *. intros. simpl in |- *. elim X; try auto. intros. right. rewrite cpoly_ap_p_zero. assumption. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational