diff options
Diffstat (limited to 'theories/Reals/Alembert.v')
| -rw-r--r-- | theories/Reals/Alembert.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index c87053772..e86a4d003 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -14,6 +14,7 @@ Require Rseries. Require SeqProp. Require PartSum. Require Max. +Import R_scope. (***************************************************) (* Various versions of the criterion of D'Alembert *) @@ -544,4 +545,4 @@ Unfold Rdiv; Apply Rmult_lt_pos. Assumption. Apply Rlt_Rinv; Apply Rabsolu_pos_lt. Red; Intro H7; Rewrite H7 in r; Elim (Rlt_antirefl ? r). -Qed.
\ No newline at end of file +Qed. |