proposition: Lemma x_is_SeqLimit_G : forall x : R1, SeqLimit (inj_Q_G_as_CauchySeq x) x.
proof: Proof. intros. unfold SeqLimit in |- *. intros e H. unfold inj_Q_G_as_CauchySeq in |- *. unfold CS_seq in |- *. cut {n : nat | (inj_Q R1 (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_leEq_trans with (e1 := inj_Q R1 ((start_r x[-]start_l x)[/]nring (S (S (N + 3)))[//] nringS_ap_zero Q_as_COrdField (S (N + 3)))). apply less_leEq. apply less_transitive_unfolded with (y := inj_Q R1 ((start_r x[-]start_l x)[/]nring (R:=Q_as_COrdField) (S N)[//] nringS_ap_zero _ N)). apply inj_Q_less. apply mult_cancel_less with (nring (R:=Q_as_COrdField) (S (S (N + 3)))[*]nring (S N)). apply mult_resp_pos. apply pos_nring_S. apply pos_nring_S. rstepl ((start_r x[-]start_l x)[*]nring (S N)). rstepr ((start_r x[-]start_l x)[*]nring (S (S (N + 3)))). apply mult_resp_less_lft. apply nring_less. apply -> Nat.succ_lt_mono. apply Nat.lt_succ_r. apply Nat.le_add_r. apply shift_zero_less_minus. apply l_less_r. astepl (inj_Q R1 (start_r x[-]start_l x)[/]nring (S N)[//]nringS_ap_zero R1 N). 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 mult_cancel_lft with (z := nring (R:=R1) (S N)). apply nringS_ap_zero. rstepl (inj_Q R1 (start_r x[-]start_l x)). astepr (inj_Q R1 (nring (S N))[*] inj_Q R1 ((start_r x[-]start_l x)[/]nring (S N)[//] nringS_ap_zero Q_as_COrdField N)). astepr (inj_Q R1 (nring (S N)[*] ((start_r x[-]start_l x)[/]nring (S N)[//] nringS_ap_zero Q_as_COrdField N))). apply inj_Q_wd. rational. apply AbsSmall_leEq_trans with (e1 := inj_Q R1 ((start_r x[-]start_l x)[/]nring (S m)[//] nringS_ap_zero Q_as_COrdField m)). apply inj_Q_leEq. apply mult_cancel_leEq with (nring (R:=Q_as_COrdField) (S (S (N + 3)))[*]nring (S m)). apply mult_resp_pos. apply pos_nring_S. apply pos_nring_S. rstepl ((start_r x[-]start_l x)[*]nring (S (S (N + 3)))). rstepr ((start_r x[-]start_l x)[*]nring (S m)). apply mult_resp_leEq_lft. apply nring_leEq. apply le_n_S. assumption. apply less_leEq. apply shift_zero_less_minus. apply l_less_r. apply G_conversion_rate_resp_x. apply Nat.le_trans 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.Q_in_CReals