proposition: Lemma poly_apzero : forall f : RX, f [#] [0] -> {c : R | f ! c [#] [0]}.
proof: Proof. intros f H0. elim (Cpoly_ex_degree _ f). intro n. intro H1. cut (distinct1 (fun i : nat => nring i:R)). intro H2. elim (Cpoly_choose_apzero _ (fun i : nat => nring i:R) H2 f n H1 H0). intro i. intros. exists (nring i:R). auto. unfold distinct1 in |- *. intros. apply nring_different; auto. Qed.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation