proposition: Lemma RisReals : is_CReals ROrdField RLim.
proof: Proof. constructor. intros [s hs]. unfold SeqLimit. unfold RLim. intros e e0. simpl. destruct (R_complete s ((cauchy_prop_cauchy_crit (Build_CauchySeq ROrdField s hs) s hs))). unfold Rseries.Un_cv in u. simpl in *. destruct (hs (e/4)) as [N HN]. simpl. lra. exists N. intros m Hm. destruct (u (e/2)). lra. set (z:=Nat.max x0 m). rstepr (((s m[-]s N)[+](s N[-]s z))[+](s z[-]x)). apply AbsSmall_eps_div_two. apply AbsSmall_eps_div_two. stepl (e/4). apply HN; auto. change (e / 4 = e * / (0 + 1 + 1) * / (0 + 1 + 1)). field. apply AbsSmall_minus. stepl (e/4). unfold z. apply HN; eauto with *. change (e / 4 = e * / (0 + 1 + 1) * / (0 + 1 + 1)). field. assert (Hz:(z >= x0)%nat). unfold z; eauto with *. destruct (Rabs_def2 _ _ (H _ Hz)) as [A0 A1]. stepl (e/2). split; unfold cg_minus; simpl; auto with *. change (e / 2 = e * / (0 + 1 + 1)). field. intro x. exists (Z.abs_nat (up x)). unfold Z.abs_nat. elim (archimed x). destruct (up x). simpl; intros; lra. rewrite <- positive_nat_Z. intros H _. apply Rlt_le. rewrite <- R_INR_as_IR. now rewrite INR_IZR_INZ. intros I _. cut (x < 0%R). intro H; clear I. rewrite <- R_INR_as_IR. cut (0 <= INR (nat_of_P p)). intro. apply Rlt_le. lra. apply pos_INR. cut (0 <= INR (nat_of_P p)). rewrite INR_IZR_INZ. intro. change (IZR (Zneg p)) with (Ropp (IZR (Zpos p))) in I. rewrite <- positive_nat_Z in I. lra. apply pos_INR. Qed.
imports: CoRN.algebra.CSetoids CoRN.algebra.CSemiGroups CoRN.algebra.CMonoids CoRN.algebra.CGroups CoRN.tactics.CornTac CoRN.algebra.CAbGroups CoRN.algebra.CRings CoRN.algebra.CFields CoRN.algebra.COrdFields CoRN.reals.CReals Coq.Reals.RIneq Coq.Reals.Rcomplete Coq.Reals.Rlimit Coq.Reals.Rbasic_fun Coq(Lra)