diff options
| author | Maxime Dénès | 2017-06-15 11:52:19 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-15 11:52:19 +0200 |
| commit | 28c732ea340f5ac571a77a8ac26de600c29165b2 (patch) | |
| tree | 9ee6deb6ecb31c520ffb4c278560a527cb550db4 /theories/Reals | |
| parent | e710306910afc61c9a874e6020bbf35b77ffe4af (diff) | |
| parent | 7668037a8daaef7bc8f1fc3225c2e6cc26cac0aa (diff) | |
Merge PR#375: Deprecation
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/SeqProp.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 3697999f70..6a5233b643 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -150,7 +150,7 @@ Definition sequence_lb (Un:nat -> R) (pr:has_lb Un) (* Compatibility *) Notation sequence_majorant := sequence_ub (only parsing). Notation sequence_minorant := sequence_lb (only parsing). -Unset Standard Proposition Elimination Names. + Lemma Wn_decreasing : forall (Un:nat -> R) (pr:has_ub Un), Un_decreasing (sequence_ub Un pr). Proof. |