proposition: Lemma Cseq_partial_bound : forall N, exists M, forall n, (n <= N)%nat -> Cnorm (Un n) <= M.
proof: Proof. intros N. destruct (Rseq_partial_bound_max (fun n => Cnorm (Un n)) N) as (M, HM) ; exists M ; apply HM. Qed.
imports: MyReals PeanoNat Rsequence_def Rsequence_facts Rsequence_base_facts Lia Lra Complex Csequence_def