proposition: Lemma twice_inv_seq_Lim : SeqLimit (R:=IR) (fun n => Two[*]one_div_succ n) [0].
proof: Proof. red in |- *; fold (Cauchy_Lim_prop2 (fun n : nat => Two[*]one_div_succ n) [0]) in |- *. Proof. apply Cauchy_Lim_prop3_prop2. red in |- *; intro. exists (2 * S k); intros. astepr ((Two:IR) [*]one_div_succ m). apply AbsIR_imp_AbsSmall. apply leEq_wdl with ((Two:IR) [*]one_div_succ m). 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. astepl (one_div_succ (R:=IR) m[*]Two). unfold one_div_succ in |- *; simpl in |- *; fold (Two:IR) in |- *. apply shift_mult_leEq with (two_ap_zero IR). apply pos_two. unfold Snring in |- *. rstepr ([1][/] nring (S k) [*]Two[//] mult_resp_ap_zero _ _ _ (nring_ap_zero _ (S k) (sym_not_eq (O_S k))) (two_ap_zero IR)). apply recip_resp_leEq. astepl (ZeroR[*][0]); apply mult_resp_less_both; try apply leEq_reflexive. apply pos_nring_S. apply pos_two. astepl ((Two:IR) [*]nring (S k)). apply leEq_transitive with (nring (R:=IR) m). apply leEq_wdl with (nring (R:=IR) (2 * S k)). apply nring_leEq. assumption. apply nring_comm_mult. simpl in |- *; astepl (nring (R:=IR) m[+][0]); apply plus_resp_leEq_lft; apply less_leEq; apply pos_one. astepl (ZeroR[*][0]); apply mult_resp_leEq_both; try apply leEq_reflexive. apply less_leEq; apply pos_two. apply less_leEq; apply one_div_succ_pos. Qed.
imports: CoRN.reals.Max_AbsIR CoRN.algebra.Expon CoRN.algebra.CPoly_ApZero