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. intros. simpl in |- *. unfold cpoly_zero_cs in |- *. rewrite cpoly_ap_p_zero. reflexivity. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational