diff options
Diffstat (limited to 'theories/Reals/Rseries.v')
| -rw-r--r-- | theories/Reals/Rseries.v | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 9af9bdd549..7cc969afe8 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -8,7 +8,8 @@ (*i $Id$ i*) -Require Export Rderiv. +Require RealsB. +Require Rfunctions. Require Classical. Require Compare. @@ -271,9 +272,4 @@ Assumption. Apply Rabsolu_pos_lt. Apply Rinv_neq_R0. Assumption. -Qed. - - - - - +Qed.
\ No newline at end of file |