proposition: Lemma DL_sqrt_1 : forall Un, Rseq_cv Un 0 -> (fun n => sqrt (1 + Un n) - 1) = o(1).
proof: Proof. intros Un Un0. intros eps Heps. destruct (Un0 eps Heps) as (N, HUn). assert (H01 : 0 < 1) by lra. destruct (Un0 1 H01) as (N1, HUn1). exists (max N N1). intros n HNmax. unfold Rseq_constant. rewrite Rabs_R1. rewrite Rmult_1_r. apply Rle_trans with (Rabs (Un n)). apply sqrt_var_maj. unfold R_dist in *. left. assert (HN : (n >= N1)%nat). apply Nat.le_trans with (Nat.max N N1) ; intuition. generalize (HUn1 n HN) ; intros HU1. rewrite Rminus_0_r in HU1. assumption. left. assert (HN : (n >= N)%nat). apply Nat.le_trans with (Nat.max N N1) ; intuition. generalize (HUn n HN) ; intros HU1. unfold R_dist in HU1. rewrite Rminus_0_r in HU1. assumption. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics