proposition: Lemma Rseq_partial_bound : forall N, exists M, forall n, (n <= N)%nat -> Rabs (Un n) <= M.
proof: Proof. intros N. destruct (Rseq_partial_bound_max N) as [M HM]. destruct (Rseq_partial_bound_min N) as [m Hm]. exists (Rmax (Rabs m) (Rabs M)). intros n Hn. apply RmaxAbs; [apply Hm|apply HM]; assumption. Qed.
imports: Lia Rsequence_def Morphisms Setoid Lra