proposition: Lemma intervals_small'' : forall i : nat, Small[^]i[*]nring i [<=] [1].
proof: Proof. intros. apply mult_cancel_leEq with (Three[^]i:IR). apply nexp_resp_pos. apply pos_three. astepr (Three[^]i:IR). apply leEq_wdl with (nring i[*]Two[^]i:IR). 2: rstepr (nring i[*] (Small[^]i[*]Three[^]i)). 2: astepr (nring i[*] (Small[*]Three) [^]i). 2: cut (Small[*]Three [=] Two); algebra. 2: unfold Small in |- *; rational. induction i as [| i Hreci]. simpl in |- *. astepl ZeroR. apply less_leEq. apply pos_one. elim (zerop i); intro y. rewrite y. simpl in |- *. rstepl (Two:IR). rstepr (Three:IR). apply less_leEq. apply two_less_three. elim (le_lt_eq_dec _ _ (proj1 (Nat.le_succ_l _ _) y)); intros H0. apply mult_cancel_leEq with (nring i:IR). astepl (nring 0:IR). apply nring_less. auto. apply leEq_wdl with (nring (S i) [*]Two[*] (nring i[*]Two[^]i:IR)). 2: simpl in |- *; rational. apply leEq_wdr with (nring i[*]Three[*]Three[^]i:IR). 2: simpl in |- *; rational. apply leEq_transitive with (nring i[*]Three[*] (nring i[*]Two[^]i:IR)). apply mult_resp_leEq_rht. simpl in |- *. rstepl (nring i[*]Two[+] (Two:IR)). rstepr (nring i[*]Two[+] (nring i:IR)). apply plus_resp_leEq_lft. elim (le_lt_eq_dec _ _ (proj1 (Nat.le_succ_l _ _) H0)); intros H1. apply less_leEq. apply nring_less. auto. rewrite <- H1. apply leEq_reflexive. apply less_leEq. apply mult_resp_pos. astepl (nring 0:IR). apply nring_less. auto. apply nexp_resp_pos. apply pos_two. apply mult_resp_leEq_lft. auto. apply less_leEq. apply mult_resp_pos. astepl (nring 0:IR). apply nring_less. auto. apply pos_three. rewrite <- H0. rstepl (nring (R:=IR) 8). rstepr (nring (R:=IR) 9). apply nring_leEq. auto. Qed.
imports: CoRN.reals.CPoly_Contin