proposition: Theorem cauchy_gives_lub : l_u_b R1 A.
proof: Proof. intros. unfold l_u_b in |- *. exists B. split. red in |- *. intros t At. intros. case (B_limit_W ((t[-]z) [/]TwoNZ)). apply pos_div_two. apply shift_zero_less_minus. assumption. intro N. intro H0. cut (AbsSmall ((t[-]z) [/]TwoNZ) (W N[-]B)). intro H1. apply plus_cancel_less with (z := (t[-]z) [/]TwoNZ). apply less_leEq_trans with (y := W N). rstepl (t[-](t[-]z) [/]TwoNZ). cut (is_upper_bound R1 A (W N)). intro H2. red in H2. apply (H2 t At). apply plus_cancel_less with (z := (t[-]z) [/]TwoNZ[-]t). rstepl ([0]:R1). rstepr ((t[-]z) [/]TwoNZ). apply pos_div_two. apply shift_zero_less_minus. assumption. apply W_n_is_upper. apply plus_cancel_leEq_rht with (z := [--]B). astepl (W N[-]B). rstepr ((t[-]z) [/]TwoNZ). elim H1. intros H2 H3. assumption. apply H0. constructor. intros b' H. case (B_limit_V ((B[-]b') [/]TwoNZ)). apply pos_div_two. apply shift_zero_less_minus. assumption. intro N. intro H0. cut (AbsSmall ((B[-]b') [/]TwoNZ) (V N[-]B)). intros. case (A_bounds_V_n N). intro s'. set (H2 := True) in *. intros. exists s'. split. assumption. apply less_transitive_unfolded with (y := V N). apply less_leEq_trans with (y := B[-](B[-]b') [/]TwoNZ). apply plus_cancel_less with (z := [--]b'). astepl ([0]:R1). rstepr ((B[-]b') [/]TwoNZ). apply pos_div_two. apply shift_zero_less_minus. assumption. apply plus_cancel_leEq_rht with (z := [--]B). astepr (V N[-]B). rstepl ([--]((B[-]b') [/]TwoNZ)). elim H1. intros. assumption. assumption. apply H0. constructor. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon