diff options
Diffstat (limited to 'theories/Reals/Sqrt_reg.v')
| -rw-r--r-- | theories/Reals/Sqrt_reg.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index 05de0f1c6..9cf2ac003 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Ranalysis1. Require R_sqrt. @@ -293,4 +293,4 @@ Apply sqrt_positivity; Apply Rle_sym2; Exact r. Left; Exact H2. Apply Rle_sym1; Apply sqrt_positivity; Apply Rle_sym2; Exact r. Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? H1 H)). -Qed.
\ No newline at end of file +Qed. |