proposition: Lemma CS_seq_U : Cauchy_prop (fun m : nat => U m).
proof: Proof. intros. unfold Cauchy_prop in |- *. intros e H. cut {n : nat | (dstart_r[-]dstart_l[/] e[//]Greater_imp_ap _ e [0] H)[<]nring n}. intro H0. case H0. intro N. intro. exists (S (N + 3)). intros. apply AbsSmall_minus. apply AbsSmall_leEq_trans with (e1 := dstart_r[-]dstart_l[/] nring (S (S (N + 3)))[//] nringS_ap_zero R1 (S (N + 3))). apply less_leEq. apply swap_div with (z_ := Greater_imp_ap _ e [0] H). apply pos_nring_S. assumption. apply less_transitive_unfolded with (y := nring (R:=R1) N). assumption. apply nring_less. apply Nat.lt_succ_r. constructor. apply Nat.le_add_r. apply U_conversion_rate2 with (m := S (N + 3)). apply le_n_S. rewrite Nat.add_comm; apply Nat.le_add_r. assumption. apply Archimedes'. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon