proposition: Lemma poly_IR_extensional : forall p q : cpoly_cring IR, (forall x, p ! x [=] q ! x) -> p [=] q.
proof: Proof. intros. apply poly_extensional. exact char0_IR. auto. Qed.
imports: CoRN.reals.Max_AbsIR CoRN.algebra.Expon CoRN.algebra.CPoly_ApZero