proposition: Lemma nat_nondecreasing_is_cvg (u_ : nat^nat) : nondecreasing_seq u_ -> has_ubound (range u_) -> cvgn u_.
proof: Proof. move=> u_nd [l ul]. suff [N Nu] : exists N, forall n, (n >= N)%N -> u_ n = u_ N. apply/cvg_ex; exists (u_ N); rewrite -(cvg_shiftn N). rewrite [X in X @ \oo --> _](_ : _ = cst (u_ N))//; first exact: cvg_cst. by apply/funext => n /=; rewrite Nu// leq_addl. apply/not_existsP => hu. have {hu}/choice[f Hf] : forall x, (exists n, x <= n /\ u_ n > u_ x)%N. move=> x; have /existsNP[N /not_implyP[xN Nx]] := hu x. exists N; split => //; move/eqP : Nx; rewrite neq_lt => /orP[|//]. by move/u_nd : xN; rewrite le_eqVlt => /predU1P[->|//]. have uf : forall x, (x < u_ (iter x.+1 f O))%N. elim=> /= [|i ih]; first by have := Hf O => -[_]; exact: leq_trans. by have := Hf (f (iter i f O)) => -[_]; exact: leq_trans. have /ul : range u_ (u_ (iter l.+1 f O)) by exists (iter l.+1 f O). by rewrite leNgt => /negP; apply; rewrite ltEnat //=; exact: uf. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau