proposition: Lemma convergent_subseq : forall k : nat, {N_k : nat | k <= N_k | AbsSmall (one_div_succ k) (g_ N_k[-]L)}.
proof: Proof. intros. case (Pinf_unfolded2_informative sup_tail_as_Cauchy (L[+]one_div_succ k)). change (L[<]L[+]one_div_succ k) in |- *. apply shift_less_plus'. rstepl ([0]:OF). apply one_div_succ_pos. intro sN. intros. red in s. case s. intro N. intros c0. case (Psup_unfolded2_informative (tail_seq g (k + N)) (L[-]one_div_succ k)). apply less_leEq_trans with (y := L). apply shift_minus_less. apply shift_less_plus'. rstepl ([0]:OF). apply one_div_succ_pos. change (L[<=]sup_tail (k + N)) in |- *. apply L_less_sup_n. intro xj. intros. case s0. intro j. intros. exists (k + N + j). apply Nat.le_trans with (m := k + N). apply Nat.le_add_r. apply Nat.le_add_r. split. apply shift_leEq_minus. rstepl (L[-]one_div_succ k). apply leEq_wdr with (y := xj). apply less_leEq; assumption. assumption. apply shift_minus_leEq. apply leEq_transitive with (y := sN). change (CS_seq OF (tail_seq g (k + N)) j[<=]sN) in |- *. apply leEq_transitive with (y := sup (tail_seq g (k + N))). apply sup_leEq. apply leEq_wdr with (y := sup (tail_seq g N)). change (sup_tail (k + N)[<=]sup_tail N) in |- *. apply sup_tail_decrease. rewrite Nat.add_comm; apply Nat.le_add_r. apply eq_symmetric_unfolded. assumption. apply less_leEq. astepr (L[+]one_div_succ k); auto. Qed.
imports: CoRN.reals.Bridges_LUB