diff options
Diffstat (limited to 'theories/Reals/Rseries.v')
| -rw-r--r-- | theories/Reals/Rseries.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 65bf76c5f1..5f8b5d9da2 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -133,7 +133,7 @@ Section sequence. clear -Hi2pn. intros m. induction n. - rewrite plus_0_r. + rewrite<- plus_n_O. ring_simplify (sum m + (/ 2) ^ m - (/ 2) ^ m). split ; apply Rle_refl. rewrite <- plus_n_Sm. |