proposition: Lemma Rseq_unbounded_growing : Rseq_growing Un -> (~ exists M, Rseq_bound_max Un M) -> Rseq_cv_pos_infty Un.
proof: Proof. intros Hgr Hnmaj m. apply NNPP; intro Hf; apply Hnmaj. exists m; intro n. apply NNPP. intro Hff. apply Hf. apply Rnot_le_lt in Hff. exists n. intros p Hp. apply Rlt_le_trans with (Un n); [ apply Hff | apply Rge_le]. apply growing_prop. apply Hgr. apply Hp. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_usual_facts Lra