proposition: Lemma B_limit_V : forall e : R1, [0][<]e -> {N : nat | forall m : nat, N <= m -> AbsSmall e (V m[-]B)}.
proof: Proof. intros e H. cut {N : nat | forall m : nat, N <= m -> AbsSmall (e [/]TwoNZ) (V m[-]U m)}. intro H0. cut {N : nat | forall m : nat, N <= m -> AbsSmall (e [/]TwoNZ) (U m[-]B)}. intro H1. case H0. intro N1. intro H2. case H1. intro N2. intro H3. exists (N1 + N2). intros. rstepr (V m[-]U m[+](U m[-]B)). rstepl (e [/]TwoNZ[+]e [/]TwoNZ). apply AbsSmall_plus. apply H2. apply Nat.le_trans with (m := N1 + N2). apply Nat.le_add_r. assumption. apply H3. apply Nat.le_trans with (m := N1 + N2). rewrite Nat.add_comm; apply Nat.le_add_r. assumption. unfold B in |- *. cut (SeqLimit U_as_CauchySeq (Lim U_as_CauchySeq)). intro H1. red in H1. apply H1. apply pos_div_two. assumption. apply Lim_Cauchy. cut {n : nat | (Two[*](dstart_r[-]dstart_l)[/] e[//]Greater_imp_ap _ e [0] H)[<]nring n}. intro H0. case H0. intro N. intros. case (twisted_archimedean N (Three [/]TwoNZ)). apply mult_cancel_less with (z := Two:R1). apply pos_two. astepl (Two:R1). rstepr (Three:R1). apply two_less_three. intro M. intros. exists M. intros. apply AbsSmall_leEq_trans with (e1 := (Two [/]ThreeNZ)[^]m[*](dstart_r[-]dstart_l)). apply less_leEq. apply mult_cancel_less with (z := ((Three:R1) [/]TwoNZ)[^]m). apply less_leEq_trans with (y := ((Three:R1) [/]TwoNZ)[^]0). simpl in |- *. apply pos_one. apply great_nexp_resp_le. apply less_leEq. apply mult_cancel_less with (z := Two:R1). apply pos_two. rstepl (Two:R1). rstepr (Three:R1). apply two_less_three. apply Nat.le_0_l. apply less_wdl with (x := (Two[^]m[/] Three[^]m[//]nexp_resp_ap_zero m (three_ap_zero R1))[*] (dstart_r[-]dstart_l)[*] (Three[^]m[/] Two[^]m[//]nexp_resp_ap_zero m (two_ap_zero R1))). rstepl (dstart_r[-]dstart_l). apply mult_cancel_less with (z := Two[/] e[//]Greater_imp_ap _ e [0] H). apply div_resp_pos. assumption. apply pos_two. apply less_wdl with (x := Two[*](dstart_r[-]dstart_l)[/] e[//]Greater_imp_ap _ e [0] H). rstepr (((Three:R1) [/]TwoNZ)[^]m). apply less_transitive_unfolded with (y := nring (R:=R1) N). assumption. apply less_leEq_trans with (y := ((Three:R1) [/]TwoNZ)[^]M). assumption. apply great_nexp_resp_le. apply less_leEq. apply mult_cancel_less with (z := Two:R1). apply pos_two. rstepl (Two:R1). astepr (Three:R1). apply two_less_three. assumption. rational. apply bin_op_wd_unfolded. apply bin_op_wd_unfolded. apply eq_symmetric_unfolded. apply nexp_distr_div'. apply eq_reflexive_unfolded. apply eq_symmetric_unfolded. apply nexp_distr_div'. apply AbsSmall_minus. apply AbsSmall_U_V. apply Archimedes'. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon