diff options
Diffstat (limited to 'theories/Reals/Rseries.v')
| -rw-r--r-- | theories/Reals/Rseries.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 328ba27e6..57b9d3d2f 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -237,9 +237,9 @@ Section sequence. apply le_n_Sn. rewrite (IHN H6), Rplus_0_l. unfold test. - destruct Rle_lt_dec. + destruct Rle_lt_dec as [Hle|Hlt]. apply eq_refl. - now elim Rlt_not_le with (1 := r). + now elim Rlt_not_le with (1 := Hlt). destruct (le_or_lt N n) as [Hn|Hn]. rewrite le_plus_minus with (1 := Hn). |