proposition: Lemma CS_seq_bounded' : forall seq : CauchySeqR, {K : IR | [0] [<] K | forall m : nat, AbsSmall K (seq m)}.
proof: Proof. unfold CauchySeqR in |- *. intros. assert (X0 : {K : IR | [0] [<] K | {N : nat | forall m, N <= m -> AbsSmall K (seq m)}}). apply CS_seq_bounded; auto. apply (CS_proof _ seq). destruct X0 as [K1 K1_pos H1]. destruct H1 as [N H1]. exists (Max K1 (SeqBound0 seq N)). apply less_leEq_trans with K1; auto. apply lft_leEq_MAX. intros. elim (Nat.le_gt_cases N m). intros. assert (AbsSmall (R:=IR) K1 (seq m)). apply H1. auto. apply AbsSmall_leEq_trans with K1; auto. apply lft_leEq_MAX. intros. apply AbsSmall_leEq_trans with (SeqBound0 seq N). apply rht_leEq_MAX. apply AbsSmall_leEq_trans with (AbsIR (seq m)). apply SeqBound0_greater; auto. apply AbsIR_imp_AbsSmall. apply leEq_reflexive. Qed.
imports: CoRN.reals.Max_AbsIR CoRN.algebra.Expon CoRN.algebra.CPoly_ApZero