proposition: Lemma Cpoly_apzero_interval : forall f : RX, f [#] [0] -> forall a b, a [<] b -> {c : R | a [<=] c /\ c [<=] b | f ! c [#] [0]}.
proof: Proof. intros f H a b H0. assert (H1 := poly_degree_lth _ f). set (n := lth_of_poly f) in *. cut ([0] [<] (nring n:R)). intros H2. cut (nring n [#] ([0]:R)). intros H3. cut (distinct1 (fun i : nat => nring i[*]a[+] (nring n[-]nring i) [*]b[/] nring n[//]H3)). intro H4. elim (Cpoly_choose_apzero _ (fun i : nat => nring i[*]a[+] (nring n[-]nring i) [*]b[/] nring n[//]H3) H4 f n H1 H). intro i. intros H6 H7. exists (nring i[*]a[+] (nring n[-]nring i) [*]b[/] nring n[//]H3). split. apply shift_leEq_div. auto. rstepl (nring i[*]a[+] (nring n[-]nring i) [*]a). apply plus_resp_leEq_lft. apply mult_resp_leEq_lft. apply less_leEq. auto. apply shift_leEq_minus. astepl (nring (R:=R) i). apply nring_leEq. auto. apply shift_div_leEq. auto. rstepr (nring i[*]b[+] (nring n[-]nring i) [*]b). apply plus_resp_leEq. apply mult_resp_leEq_lft. apply less_leEq. auto. astepl (nring 0:R). apply nring_leEq. auto with arith. auto. unfold distinct1 in |- *. intros. unfold cf_div in |- *. apply mult_rht_resp_ap. apply zero_minus_apart. rstepl ((nring i[-]nring j) [*] (a[-]b)). apply mult_resp_ap_zero. apply minus_ap_zero. apply nring_apart. auto. apply minus_ap_zero. apply less_imp_ap. auto. apply f_rcpcl_resp_ap_zero. apply pos_ap_zero. auto. astepl (nring 0:R). apply nring_less. unfold n in |- *. generalize H; clear H1 H; case f. intro H; inversion H. intros; simpl in |- *. auto with arith. Qed.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation