diff options
Diffstat (limited to 'theories/Reals/Rlogic.v')
| -rw-r--r-- | theories/Reals/Rlogic.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v index 7bd6c916d..b9a9458c8 100644 --- a/theories/Reals/Rlogic.v +++ b/theories/Reals/Rlogic.v @@ -82,7 +82,7 @@ assert (HN: (INR N + 1 = IZR (up (/ l)) - 1)%R). apply Rle_lt_trans with (1 := H1l). apply archimed. rewrite minus_IZR. - change (IZR 2) with 2%R. + simpl. ring. assert (Hl': (/ (INR (S N) + 1) < l)%R). rewrite <- (Rinv_involutive l) by now apply Rgt_not_eq. |