proposition: Lemma Cseq_cv_bound : exists M, 0 < M /\ Cseq_bound Un M.
proof: Proof. destruct (Hu 1%R) as [N HN]; [lra|]. destruct (Cseq_partial_bound Un N) as [M HM]. exists (Rmax (1 + (Cnorm lu)) M). split. eapply Rlt_le_trans; [|apply RmaxLess1]. apply Rplus_lt_le_0_compat; [lra|apply Cnorm_pos]. intros n. destruct (le_ge_dec n N) as [He|He]. eapply Rle_trans; [apply HM; assumption|apply RmaxLess2]. eapply Rle_trans; [|apply RmaxLess1]. replace (Un n) with ((Un n - lu) + lu)%C by field. eapply Rle_trans; [apply Cnorm_triang|]. apply Rplus_le_compat. left; apply HN; assumption. apply Rle_refl. Qed.
imports: MyReals PeanoNat Rsequence_def Rsequence_facts Rsequence_base_facts Lia Lra Complex Csequence_def