proposition: Lemma Rseq_growing_constructive_limit : forall (Un : nat -> R), Rseq_growing Un -> (exists l, Rseq_cv Un l) -> {l | Rseq_cv Un l}.
proof: Proof. intros Un Hg Hl. assert (has_ub Un). destruct Hl as [l Hl]; exists l. intros x Hx; destruct Hx as [n Hn]; rewrite Hn. apply growing_ineq; assumption. apply growing_cv; assumption. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_usual_facts Lra