proposition: Lemma Rseq_unbounded_decreasing : Rseq_decreasing Un -> (~ exists M, Rseq_bound_min Un M) -> Rseq_cv_neg_infty Un.
proof: Proof. intros Hgr Hnmin m. apply NNPP; intro Hf; apply Hnmin. exists m; intro n. apply NNPP. intro Hff. apply Hf. apply Rnot_le_lt in Hff. exists n. intros p Hp. apply Rle_lt_trans with (Un n). apply decreasing_prop. apply Hgr. apply Hp. apply Hff. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_usual_facts Lra