proposition: Lemma Ccpoly_big : forall (p : RX) n, 0 < n -> monic n p -> forall Y, {X : R | forall x, X [<=] x -> Y [<=] p ! x}.
proof: Proof. intro. elim p. unfold monic in |- *. simpl in |- *. intros. elim H0. intros H1 H2. cut ([0][~=] ([1]:R)). intro. elim (H3 H1). apply ap_imp_neq. apply ap_symmetric_unfolded. apply ring_non_triv. intros c q. intros H n H0 H1 Y. elim (O_or_S n); intro y. elim y. intro m. intro y0. rewrite <- y0 in H1. elim (zerop m); intro y1. simpl in |- *. exists (Y[-]c). intros. rewrite y1 in H1. apply shift_leEq_plus'. cut (q ! x [=] [1]). intro. astepr (x[*][1]). astepr x. auto. apply monic_one with c. auto. cut (monic m q). intro H2. elim (Cbigger [0] (Y[-]c)). intro Y'. intros H3 H4. elim (H m y1 H2 Y'). intro X'. intro H5. simpl in |- *. elim (Cbigger [1] X'). intro X. intros H6 H7. exists X. intros. apply shift_leEq_plus'. apply leEq_transitive with ([1][*]Y'). astepr Y'. auto. apply mult_resp_leEq_both; auto. apply less_leEq. apply pos_one. apply leEq_transitive with X; auto. change (Y' [<=] q ! x) in |- *. apply H5. apply leEq_transitive with X; auto. apply monic_cpoly_linear with c; auto. rewrite <- y in H0. elim (Nat.lt_irrefl _ H0). Qed.
imports: CoRN.reals.IVT