proposition: Lemma poly_c_apzero : forall a : R, _C_ a [#] [0] -> a [#] [0].
proof: Proof. intros. cut (_C_ a [#] _C_ [0]). intro H0. generalize (csf_strext _ _ _ _ _ H0); auto. Hint Resolve c_zero: algebra. astepr ([0]:RX). auto. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational