diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2013-12-03 16:43:14 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2013-12-03 16:43:14 +0100 |
| commit | 943133d5a47ce4663a9b77a03b36c7c87c78d886 (patch) | |
| tree | 6321ab6fab78b5fb723310096be3eaba9ce753a1 /theories/Reals/Rseries.v | |
| parent | aca9c227772e3765833605866ac413e61a98d04a (diff) | |
Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.
Diffstat (limited to 'theories/Reals/Rseries.v')
| -rw-r--r-- | theories/Reals/Rseries.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 3c10725bd..a5e4f8f7e 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -108,7 +108,7 @@ Section sequence. intros n H4. unfold R_dist. rewrite Rabs_left1, Ropp_minus_distr. - apply Rplus_lt_reg_r with (Un n - eps). + apply Rplus_lt_reg_l with (Un n - eps). apply Rlt_le_trans with (Un N). now replace (Un n - eps + (l - Un n)) with (l - eps) by ring. replace (Un n - eps + eps) with (Un n) by ring. @@ -171,7 +171,7 @@ Section sequence. rewrite H1. apply Rle_trans with (1 := proj2 (Hsum n)). apply Rlt_le. - apply Rplus_lt_reg_r with ((/2)^n - 1). + apply Rplus_lt_reg_l with ((/2)^n - 1). now ring_simplify. exists 0. now exists O. @@ -202,7 +202,7 @@ Section sequence. refine (False_ind _ (Rle_not_lt _ _ (H (l - eps) _) _)). intros x (n, H1). now rewrite H1. - apply Rplus_lt_reg_r with (eps - l). + apply Rplus_lt_reg_l with (eps - l). now ring_simplify. assert (Rabs (/2) < 1). @@ -247,7 +247,7 @@ Section sequence. rewrite Hs, Rplus_0_l. set (k := (N + (n - N))%nat). apply Rlt_le. - apply Rplus_lt_reg_r with ((/2)^k - (/2)^N). + apply Rplus_lt_reg_l with ((/2)^k - (/2)^N). now ring_simplify. apply Rle_trans with (sum N). rewrite le_plus_minus with (1 := Hn). |