proposition: Lemma Cauchy_Lim_recip : forall seq y, Cauchy_Lim_prop2 seq y -> forall seq_ y_, Cauchy_Lim_prop2 (fun n : nat => [1][/] seq n[//]seq_ n) ([1][/] y[//]y_).
proof: Proof. intros seq y H Hn Hy. red in |- *; red in H. intros eps He. cut {n0 : nat | forall n : nat, n0 <= n -> AbsIR y [/]TwoNZ [<=] AbsIR (seq n)}. intro H0. elim H0; clear H0; intros n0 Hn0. cut ([0] [<] eps [/]TwoNZ[*] (AbsIR y[*]AbsIR y)). intro H0. elim (H _ H0); clear H. intros N HN. exists (Nat.max N n0). intros. apply AbsIR_imp_AbsSmall. apply leEq_wdl with (([1][/] _[//]AbsIR_resp_ap_zero _ (Hn m)) [*] ([1][/] _[//]AbsIR_resp_ap_zero _ Hy) [*]AbsIR (seq m[-]y)). rstepr ((Two[/] _[//]AbsIR_resp_ap_zero _ Hy) [*] ([1][/] _[//]AbsIR_resp_ap_zero _ Hy) [*] (eps [/]TwoNZ[*] (AbsIR y[*]AbsIR y))). apply mult_resp_leEq_both. astepl (ZeroR[*][0]); apply mult_resp_leEq_both; try apply leEq_reflexive. apply less_leEq; apply recip_resp_pos; apply AbsIR_pos; apply Hn. apply less_leEq; apply recip_resp_pos; apply AbsIR_pos; apply Hy. apply AbsIR_nonneg. apply mult_resp_leEq_rht. rstepr ([1][/] _[//] div_resp_ap_zero_rev _ _ _ (two_ap_zero _) (AbsIR_resp_ap_zero _ Hy)). apply recip_resp_leEq. apply pos_div_two; apply AbsIR_pos; apply Hy. apply Hn0. apply Nat.le_trans with (Nat.max N n0); auto with arith. apply less_leEq; apply recip_resp_pos; apply AbsIR_pos; apply Hy. apply AbsSmall_imp_AbsIR. apply HN. apply Nat.le_trans with (Nat.max N n0); auto with arith. apply eq_transitive_unfolded with (AbsIR ([1][/] _[//]Hn m) [*]AbsIR ([1][/] _[//]Hy) [*]AbsIR (y[-]seq m)). repeat apply mult_wd; apply eq_symmetric_unfolded. apply AbsIR_recip. apply AbsIR_recip. apply AbsIR_minus. apply eq_transitive_unfolded with (AbsIR (([1][/] _[//]Hn m) [*] ([1][/] _[//]Hy) [*] (y[-]seq m))). eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_wdl. apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply AbsIR_wd. rational. astepl (ZeroR[*][0]); apply mult_resp_less_both; try apply leEq_reflexive. apply pos_div_two; assumption. astepl (ZeroR[*][0]); apply mult_resp_less_both; try apply leEq_reflexive; apply AbsIR_pos; apply Hy. cut {n0 : nat | forall n : nat, n0 <= n -> AbsSmall (AbsIR y [/]TwoNZ) (seq n[-]y)}. 2: apply H. 2: eapply less_wdr. 3: apply AbsIR_div_two. 2: apply AbsIR_pos. 2: apply div_resp_ap_zero_rev; apply Hy. intro H0. elim H0; intros n0 Hn0; clear H0; exists n0; intros. apply leEq_transitive with (AbsIR y[-]AbsIR (seq n[-]y)). apply shift_leEq_minus; apply shift_plus_leEq'. rstepr (AbsIR y [/]TwoNZ). apply AbsSmall_imp_AbsIR. apply Hn0; assumption. apply weird_triangleIR. Qed.
imports: CoRN.reals.OddPolyRootIR