proposition: Lemma cpoly_p_plus_ap_p : forall p q, cpoly_plus_cs p q [#] p -> q [#] cpoly_zero.
proof: Proof. intros. apply cpoly_plus_q_ap_q with p. apply ap_wdl_unfolded with (cpoly_plus_cs p q). assumption. apply cpoly_plus_commutative. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational