diff options
Diffstat (limited to 'theories/Reals/Rfunctions.v')
| -rw-r--r-- | theories/Reals/Rfunctions.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index af5fda9d3d..b283b9fd8e 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -388,6 +388,7 @@ Rewrite Rabsolu_Rinv; Auto. Rewrite <- Rinv_pow; Auto. Rewrite Pow_Rabsolu; Auto. Rewrite H'0; Rewrite Rabsolu_right; Auto with real. +Apply Rle_ge; Auto with real. Apply Rlt_pow; Auto with arith. Rewrite Rabsolu_Rinv; Auto. Apply Rlt_monotony_contra with z := (Rabsolu r). |