proposition: Theorem nonarchemaedian_bound_for_Lim : forall (IR : CReals) (g : CauchySeq IR), {H : IR | [0][<]H | AbsSmall H (Lim g)}.
proof: Proof. intros. case (CS_seq_bounded IR (CS_seq IR g) (CS_proof IR g)). intro K. set (H := True) in *. intros H0 H1. case H1. intro M. intro H2. exists ([1][+]K). apply plus_resp_pos. apply pos_one. apply leEq_not_eq. apply (AbsSmall_nonneg IR K (CS_seq IR g M)). apply H2. constructor. apply ap_symmetric_unfolded; apply pos_ap_zero; auto. cut (SeqLimit g (Lim g)). intro H3. red in H3. case (H3 [1]). apply pos_one. intro N. intros. rstepr (Lim g[-]CS_seq IR g (N + M)[+]CS_seq IR g (N + M)). apply AbsSmall_plus. apply AbsSmall_minus. apply a. apply Nat.le_add_r. apply H2. rewrite Nat.add_comm; apply Nat.le_add_r. apply Lim_Cauchy. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism