proposition: Theorem lubp_gives_Cauchy : SeqLimit g L.
proof: Proof. red in |- *. intros e H. case (is_Archimedes' ((Two[/] e[//]Greater_imp_ap _ e [0] H)[-][1])). intro k. intros. case (pg (e [/]FourNZ)). apply div_resp_pos. apply pos_four. assumption. intro N1. intros. case (convergent_subseq (N1 + k)). intro Nk. intros. elim a0. intros. exists Nk. intros. change (AbsSmall e (g_ m[-]L)) in |- *. rstepl (e [/]TwoNZ[+]e [/]TwoNZ). rstepr (g_ m[-]g_ Nk[+](g_ Nk[-]L)). apply AbsSmall_plus. rstepl (e [/]FourNZ[+]e [/]FourNZ). rstepr (g_ m[-]g_ N1[+](g_ N1[-]g_ Nk)). apply AbsSmall_plus. apply a. apply Nat.le_trans with (m := Nk). apply Nat.le_trans with (m := N1 + k). apply Nat.le_add_r. assumption. assumption. apply AbsSmall_minus. apply a. apply Nat.le_trans with (m := N1 + k). apply Nat.le_add_r. assumption. apply AbsSmall_leEq_trans with (e1 := one_div_succ (R:=OF) (N1 + k)). unfold one_div_succ in |- *. unfold Snring in |- *. apply shift_div_leEq. apply pos_nring_S. cut (e [/]TwoNZ[#][0]). intro H3. apply shift_leEq_mult' with H3. apply pos_div_two. assumption. rstepl (Two[/] e[//]Greater_imp_ap _ e [0] H). change ((Two[/] e[//]Greater_imp_ap OF e [0] H)[<=]nring (N1 + k)[+][1]) in |- *. apply shift_leEq_plus. apply leEq_transitive with (y := nring (R:=OF) k). apply less_leEq; assumption. apply nring_leEq. rewrite Nat.add_comm; apply Nat.le_add_r. apply Greater_imp_ap. apply pos_div_two. assumption. assumption. Qed.
imports: CoRN.reals.Bridges_LUB