proposition: Lemma Rseq_partial_bound_max : forall N, exists M, forall n, (n <= N)%nat -> Un n <= M.
proof: Proof. induction N. exists (Un 0). intros n Hn; inversion Hn as [H|H]; apply Rle_refl. destruct IHN as [M IHN]. exists (Rmax M (Un (S N))). intros n Hn. destruct (le_lt_eq_dec n (S N)) as [He|He]; try assumption. eapply Rle_trans; [apply IHN|apply RmaxLess1]. apply Nat.lt_succ_r; assumption. rewrite He; apply RmaxLess2. Qed.
imports: Lia Rsequence_def Morphisms Setoid Lra