diff options
Diffstat (limited to 'theories/Reals/SeqSeries.v')
| -rw-r--r-- | theories/Reals/SeqSeries.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index 0d4bfbfad..14d438077 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -21,6 +21,7 @@ Require Export Rsigma. Require Export Rprod. Require Export Cauchy_prod. Require Export Alembert. +Import R_scope. (**********) Lemma sum_maj1 : (fn:nat->R->R;An:nat->R;x,l1,l2:R;N:nat) (Un_cv [n:nat](SP fn n x) l1) -> (Un_cv [n:nat](sum_f_R0 An n) l2) -> ((n:nat)``(Rabsolu (fn n x))<=(An n)``) -> ``(Rabsolu (l1-(SP fn N x)))<=l2-(sum_f_R0 An N)``. |