proposition: Lemma poly_apzero_IR : forall f : cpoly_cring IR, f [#] [0] -> {c : IR | f ! c [#] [0]}.
proof: Proof. intros. apply poly_apzero. exact char0_IR. auto. Qed.
imports: CoRN.reals.Max_AbsIR CoRN.algebra.Expon CoRN.algebra.CPoly_ApZero