proposition: Theorem expand_Q_R : forall (x : R_COrdField') e, [0] [<] e -> forall N, (forall m, N <= m -> AbsSmall (e [/]FourNZ) (CS_seq F x m[-]CS_seq F x N)) -> forall m, N <= m -> AbsSmall (inject_Q e) (inject_Q (CS_seq F x m) [-]x).
proof: Proof. intros x e H N H0 m H1. split. apply less_leEq. simpl in |- *. unfold Rlt in |- *. exists N. exists (e [/]ThreeNZ). apply pos_div_three. assumption. intros. change (e [/]ThreeNZ [<=] CS_seq F (inject_Q (CS_seq F x m) [-]x) n[-][--]e) in |- *. apply plus_cancel_leEq_rht with (R := F) (z := [--]e). rstepl ( [--] (Two[*]e [/]ThreeNZ)). rstepr (CS_seq F (inject_Q (CS_seq F x m) [-]x) n). cut (AbsSmall (e [/]FourNZ) (CS_seq F x m[-]CS_seq F x N)). intro H3. elim H3. intros H4 H5. cut (AbsSmall (e [/]FourNZ) (CS_seq F x n[-]CS_seq F x N)). intro H6. elim H6. intros H7 H8. change ( [--] (Two[*]e [/]ThreeNZ) [<=] CS_seq F x m[-]CS_seq F x n) in |- *. rstepl ( [--] (e [/]ThreeNZ) [+][--] (e [/]ThreeNZ)). rstepr (CS_seq F x m[-]CS_seq F x N[+] (CS_seq F x N[-]CS_seq F x n)). apply plus_resp_leEq_both. apply leEq_transitive with ( [--] (e [/]FourNZ)); auto. apply inv_resp_leEq. apply mult_cancel_leEq with (nring (R:=F) 12). apply nring_pos. auto with arith. rstepl ([0][+]Three[*]e); rstepr (e[+]Three[*]e). apply plus_resp_leEq; apply less_leEq; auto. apply inv_cancel_leEq. rstepl (CS_seq F x n[-]CS_seq F x N). rstepr (e [/]ThreeNZ). apply leEq_transitive with (e [/]FourNZ); auto. apply mult_cancel_leEq with (nring (R:=F) 12). apply nring_pos. auto with arith. rstepl ([0][+]Three[*]e); rstepr (e[+]Three[*]e). apply plus_resp_leEq; apply less_leEq; auto. apply H0. assumption. apply H0. assumption. apply less_leEq. simpl in |- *. unfold Rlt in |- *. exists N. exists (e [/]ThreeNZ). apply pos_div_three. assumption. intros. change (e [/]ThreeNZ [<=] e[-]CS_seq F (inject_Q (CS_seq F x m) [-]x) n) in |- *. apply plus_cancel_leEq_rht with (R := F) (z := [--]e). rstepl ( [--] (Two[*]e [/]ThreeNZ)). rstepr ( [--] (CS_seq F (inject_Q (CS_seq F x m) [-]x) n)). apply inv_resp_leEq. cut (AbsSmall (e [/]FourNZ) (CS_seq F x m[-]CS_seq F x N)). intro. elim H3. intros H4 H5. cut (AbsSmall (e [/]FourNZ) (CS_seq F x n[-]CS_seq F x N)). intro. elim H6. intros H7 H8. change (CS_seq F x m[-]CS_seq F x n [<=] Two[*]e [/]ThreeNZ) in |- *. rstepr (e [/]ThreeNZ[+]e [/]ThreeNZ). rstepl (CS_seq F x m[-]CS_seq F x N[+] (CS_seq F x N[-]CS_seq F x n)). apply plus_resp_leEq_both. apply leEq_transitive with (e [/]FourNZ); auto. apply mult_cancel_leEq with (nring (R:=F) 12). apply nring_pos. auto with arith. rstepl ([0][+]Three[*]e); rstepr (e[+]Three[*]e). apply plus_resp_leEq; apply less_leEq; auto. apply inv_cancel_leEq. rstepr (CS_seq F x n[-]CS_seq F x N). apply leEq_transitive with ( [--] (e [/]FourNZ)); auto. apply inv_resp_leEq. apply mult_cancel_leEq with (nring (R:=F) 12). apply nring_pos. auto with arith. rstepl ([0][+]Three[*]e); rstepr (e[+]Three[*]e). apply plus_resp_leEq; apply less_leEq; auto. apply H0. assumption. apply H0. assumption. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals