proposition: Lemma poly_eq_zero : forall p : RX, p [=] cpoly_zero R -> forall x, p ! x [=] [0].
proof: Proof. intros. astepl (cpoly_zero R) ! x. change ([0] ! x [=] [0]) in |- *. algebra. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational