proposition: Lemma CS_seq_G : forall x : R1, Cauchy_prop (fun m : nat => G x m).
proof: Proof. intros. unfold Cauchy_prop in |- *. intros e H. cut {n : nat | (start_r x[-]start_l x[/] 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 (start_r x[-]start_l x[/] nring (S (S (N + 3)))[//] nringS_ap_zero Q_as_COrdField (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 (nring (R:=Q_as_COrdField) N). assumption. apply nring_less. apply Nat.lt_succ_r. constructor. apply Nat.le_add_r. apply G_conversion_rate2 with (m := S (N + 3)). apply le_n_S. rewrite Nat.add_comm; apply Nat.le_add_r. assumption. apply Q_is_archemaedian. Qed.
imports: CoRN.reals.Q_in_CReals