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