proposition: Lemma is_lim_seq_INR : is_lim_seq INR p_infty.
proof: Proof. apply is_lim_seq_spec. move => M. suff Hm : 0 <= Rmax 0 M. exists (S (nfloor (Rmax 0 M) Hm)) => n Hn. apply Rlt_le_trans with (2 := le_INR _ _ Hn). rewrite /nfloor S_INR. case: nfloor_ex => {n Hn} /= n Hn. apply Rle_lt_trans with (1 := Rmax_r 0 M). by apply Hn. apply Rmax_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy