proposition: Lemma filterlim_Rbar_loc_seq : forall x, filterlim (Rbar_loc_seq x) eventually (Rbar_locally' x).
proof: Proof. intros x P. unfold Rbar_loc_seq. case: x => /= [x | | ] [delta Hp]. case: (nfloor_ex (/delta)) => [ | N [_ HN]]. by apply Rlt_le, Rinv_0_lt_compat, delta. exists N => n Hn. apply Hp ; simpl. rewrite /ball /= /AbsRing_ball /abs /minus /plus /opp /=. ring_simplify (x + / (INR n + 1) + - x). rewrite Rabs_pos_eq. rewrite -(Rinv_involutive delta). apply Rinv_lt_contravar. apply Rmult_lt_0_compat. apply Rinv_0_lt_compat. by apply delta. exact: INRp1_pos. apply Rlt_le_trans with (1 := HN). by apply Rplus_le_compat_r, le_INR. by apply Rgt_not_eq, delta. by apply Rlt_le, RinvN_pos. apply Rgt_not_eq, Rminus_lt_0. ring_simplify. by apply RinvN_pos. case: (nfloor_ex (Rmax 0 delta)) => [ | N [_ HN]]. by apply Rmax_l. exists (S N) => n Hn. apply Hp. apply Rle_lt_trans with (1 := Rmax_r 0 _). apply Rlt_le_trans with (1 := HN). rewrite -S_INR ; by apply le_INR. case: (nfloor_ex (Rmax 0 (-delta))) => [ | N [_ HN]]. by apply Rmax_l. exists (S N) => n Hn. apply Hp. rewrite -(Ropp_involutive delta). apply Ropp_lt_contravar. apply Rle_lt_trans with (1 := Rmax_r 0 _). apply Rlt_le_trans with (1 := HN). rewrite -S_INR ; by apply le_INR. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub