proposition: Lemma str_comparison : forall y, convergent y -> {k : nat | forall n, k <= n -> AbsIR (x n) [<=] y n} -> convergent x.
proof: Proof. intros y H H0. elim H0; intros k Hk. red in |- *; red in |- *; intros. cut {N : nat | k < N /\ (forall m : nat, N <= m -> AbsSmall e (seq_part_sum y m[-]seq_part_sum y N))}. intros H2. elim H2; clear H2. intros N HN; elim HN; clear HN; intros HN' HN. exists N; intros. apply AbsIR_imp_AbsSmall. apply leEq_transitive with (seq_part_sum y m[-]seq_part_sum y N). apply leEq_transitive with (Sum N (pred m) (fun n : nat => AbsIR (x n))). apply leEq_wdl with (AbsIR (Sum N (pred m) x)). 2: apply AbsIR_wd; apply eq_symmetric_unfolded; apply seq_part_sum_n; auto. 2: apply Nat.lt_le_trans with N; auto; apply Nat.le_lt_trans with k; auto with arith. apply triangle_SumIR. rewrite (Nat.lt_succ_pred k m); auto with arith. apply Nat.lt_le_trans with N; auto. eapply leEq_wdr. 2: apply eq_symmetric_unfolded; apply seq_part_sum_n; auto. 2: apply Nat.le_lt_trans with k; auto with arith; apply Nat.lt_le_trans with N; auto. apply Sum_resp_leEq. rewrite (Nat.lt_succ_pred k m); auto with arith. apply Nat.lt_le_trans with N; auto. intros. apply Hk; apply Nat.le_trans with N; auto with arith. eapply leEq_transitive. apply leEq_AbsIR. apply AbsSmall_imp_AbsIR. apply HN; assumption. rename X into H1. elim (H _ (pos_div_two _ _ H1)). intros N HN; exists (S (Nat.max N k)). cut (N <= Nat.max N k); [ intro | apply Nat.le_max_l ]. cut (k <= Nat.max N k); [ intro | apply Nat.le_max_r ]. split. auto with arith. intros. rstepr (seq_part_sum y m[-]seq_part_sum y N[+] (seq_part_sum y N[-]seq_part_sum y (S (Nat.max N k)))). rstepl (e [/]TwoNZ[+]e [/]TwoNZ). apply AbsSmall_plus. apply HN; apply Nat.le_trans with (Nat.max N k); auto with arith. apply AbsSmall_minus; apply HN; auto with arith. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)